A Sequent Calculus for Answer Set Entailment

Abstract

Answer Set Programming (ASP) is a popular nonmonotonic formalism used for common-sense reasoning and problem-solving based on stable model semantics. Equilibrium logic is a generalisation of ASP for arbitrary propositional theories and thus provides a logical characterisation of the nonmonotonic stable model semantics. In difference to classical logic, which can be defined via proof or model theory, nonmonotonic reasoning formalisms are defined via their models exclusively. Equilibrium logic is no exception here, as it has no proper proof-theoretic axiomatisation. Besides this being a theoretical imbalance, it also has consequences regarding notions of justification and explainability. In this work, we fill this gap by providing a sequent calculus for answer set entailment. Our calculus builds upon ideas from existing calculi for other nonmonotonic formalisms and utilises calculi for the logic of here and there, which is the underlying base logic of equilibrium logic. We show that the calculus is sound and complete and discuss pitfalls as well as alternative axiomatisations. Finally, we address how our approach can be of use for explainability in ASP.