Set-like operations on propositional logic programs
Composition and decomposition of logic programs have been studied extensively in the context of modularity, and decomposing a program along the dependency structure of its atoms --- by strata or strongly connected components in datalog, and by splitting sets in the non-monotonic setting of answer set programming --- is standard practice. All of these approaches operate on the level of rule sets: programs are cut along dependencies between atoms, while the internal structure of the individual rules remains untouched. In this paper, we complement this picture by a finer-grained algebra. We introduce set-like operations on (propositional Horn) logic programs --- body-union, body-intersection, body-complement, body-subtraction, body-symmetric-difference, and body-power-set --- which manipulate rule bodies in analogy to the corresponding set operations, and we study their algebraic laws and their interaction with sequential composition and the least model semantics. Our main technical result is a decomposition theorem in this algebra: every minimalist program --- containing at most one rule for each rule head --- is the body-union of Krom programs consisting only of rules with at most one body atom, in such a way that its least model is the intersection of the least models of these components; for arbitrary programs we obtain corresponding approximations. Since Krom programs are algebraically better behaved than arbitrary programs --- composition is associative and distributes from the left --- this may support decomposition-based reasoning and provides a basis for compositional program construction.