Sequential Composition of Propositional Horn Theories

Rule-based reasoning is an essential part of human intelligence prominently formalized in artificial intelligence research via Horn theories. Describing complex objects as the composition of elementary ones is a common strategy in computer science and science in general. Recently, the author introduced the sequential composition of Horn logic programs for syntactic program composition and decomposition in the context of logic-based analogical reasoning and learning. This paper contributes to the foundations of logic programming, knowledge representation, and database theory by studying the sequential composition of propositional Horn theories. Specifically, we show that the notion of composition gives rise to a family of finite magmas and algebras, baptized {\em Horn magmas} and {\em Horn algebras} in this paper. On the semantic side, we show that the van Emden-Kowalski immediate consequence operator of a theory can be represented via composition, which allows us to compute its least model semantics without any explicit reference to operators. This bridges the conceptual gap between the syntax and semantics of a propositional Horn theory in a mathematically satisfactory way. Moreover, it gives rise to an algebraic meta-calculus for propositional Horn theories. In a broader sense, this paper is a first step towards an algebra of rule-based logical theories and in the future we plan to adapt and generalize the methods of this paper to wider classes of theories, most importantly to first-, and higher-order logic programs, and non-monotonic logic programs under the stable model or answer set semantics and extensions thereof.