Sequential composition of answer set programs

Non-monotonic reasoning is an essential part of human intelligence prominently formalized in artificial intelligence research via answer set programming. In this paper, we introduce the sequential composition of answer set programs. We show that the notion of composition gives rise to a family of finite program algebras, baptized ASP algebras in this paper. Interestingly, we can derive algebraic formulas for the syntactic representation of the well-known Faber-Leone-Pfeifer-, and Gelfond-Lifschitz reducts. On the semantic side, we show that the immediate consequence operator of a program can be represented via composition, which allows us to compute the least model semantics of Horn programs without any explicit reference to operators. As a result, we can characterize answer sets algebraically, which bridges the conceptual gap between the syntax and semantics of an answer set program in a mathematically satisfactory way, and which provides an algebraic characterization of strong and uniform equivalence. Moreover, it gives rise to an algebraic meta-calculus for answer set programs. In a broader sense, this paper is a first step towards an algebra of answer set programs and in the future we plan to lift the methods of this paper to wider classes of programs, most importantly to higher-order and disjunctive programs and extensions thereof.