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.
翻译:目前缺乏一个用于组合与分解逻辑程序的系统性代数框架,这限制了以模块化方式分析和构建程序的能力。本文针对(命题Horn)逻辑程序引入了集合类操作,支持对规则体进行结构化处理。我们的主要技术成果表明:程序可被分解为更简单的组件,使得其最小模型语义能够从这些组件的语义中重建或近似得到。特别地,我们证明了每个最小程序都可分解为Krom程序(仅包含至多一个体原子的规则),使其最小模型能够通过各组件的最大模型计算得出。对于任意程序,我们获得了相应的近似结果。这些成果为逻辑程序提供了新的代数视角,并为组合推理与程序构建奠定了基础。