Set-like operations on propositional logic programs
Provides a foundational algebraic framework for compositional reasoning in logic programming, benefiting researchers in knowledge representation and program analysis.
The paper introduces set-like operations for propositional Horn logic programs, enabling modular composition and decomposition. It proves that every minimalist program can be decomposed into Krom programs, allowing reconstruction of its least model from components, with approximation results for arbitrary programs.
A systematic algebraic framework for composing and decomposing logic programs is currently missing, limiting our ability to analyze and construct programs in a modular way. In this paper, we introduce set-like operations for (propositional Horn) logic programs that allow for a structured manipulation of rule bodies. Our main technical result shows that programs can be decomposed into simpler components in such a way that their least model semantics can be reconstructed or approximated from the semantics of these components. In particular, we prove that every minimalist program can be decomposed into Krom programs -- consisting only of rules with at most one body atom -- such that its least model can be computed from the least models of its components. For arbitrary programs, we obtain corresponding approximation results. These results provide a new algebraic perspective on logic programs and lay the groundwork for compositional reasoning and program construction.