Set-like operations on propositional logic programs

TL;DR

This paper introduces set-like algebraic operations for propositional logic programs, enabling modular decomposition and reconstruction of programs' semantics, particularly for minimalist and Krom programs.

Contribution

It provides a novel algebraic framework for decomposing logic programs into simpler components while preserving their least model semantics.

Findings

Programs can be decomposed into Krom components with computable least models.

Decomposition allows for approximating semantics of arbitrary programs.

Provides a foundation for modular reasoning in logic programming.

Abstract

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.