Reformulating the situation calculus and the event calculus in the general theory of stable models and in answer set programming (Q2887086)

Given a formula of first-order logic, the class of all its models can be computationally hostile, and two main ideas have emerged for selecting a useful but friendly subclass. One gives rise to the minimal models of the formula, and the other to its stable models. These two classes are not the same; neither need be included in the other. In recent years, some attention has been given to studying conditions in which they agree. An important step in that direction was recently taken by \textit{H. Zhang}, \textit{Y. Zhang}, \textit{M. Ying} and \textit{Y. Zhou} [``Translating first-order theories into logic programs'', in: Proceedings of the twenty-second international joint conference on artificial intelligence, Barcelona, Spain, July 2011. Menlo Park, CA: AAAI Press/International Joint Conferences on Artificial Intelligence. 1126--1131 (2011; \url{doi:10.5591/978-1-57735-516-8/IJCAI11-192})], who showed that the minimal models of an arbitrary first-order formula are just the stable models of a certain syntactic transformation of its negation-normal form.NEWLINENEWLINEThe paper under review takes another important step. It identifies a set of `canonical' formulae whose minimal and stable models actually coincide. The delineation of this set is made possible by a recent result (obtained in variant but essentially equivalent forms by several investigators) that we may redefine the stable models of a formula as those satisfying both it and a certain syntactically constructed second-order formula, thus bypassing the original fixpoint construction of Gelfond and Lifschitz and bringing it much closer in form to that for defining the minimal models. In addition, the authors identify another set of first-order formulae, called `almost universal', for which they have an algorithm for conversion (preserving stable models) into logic programs that are amenable to existing answer-set program (ASP) solvers. Finally, it is shown that the situation and event calculi may be expressed using only formulae that are both canonical and almost universal, so that those calculi can be computed with the ASP solvers.