First-order answer set programming and classical first-order logic

Abstract

Answer Set Programming (ASP) is a form of declarative programming oriented towards difficult and primarily NP-hard search problems. Generally speaking, an ASP search problem is formulated as a theory of some language of formal logic. The formalization is designed in such a way that the problem description is usually separate from the problem instance. Thus, once a particular encoding of a problem instance is combined with the problem description, it results in some theory of formal logic whose models (under a particular semantics) corresponds to a solution of the problem instance. This thesis is about the translation of ASP programs into classical first-order logic theories. Viewed in the context of expressing logic programs with variables into (classical) first-order logic, work of this direction goes all the way back to Clark who gave us what is now called the Clark's completion semantics, on which this work is based. This work modifies the Clark's completion in such a way that the models of the modified completion corresponds exactly to the answer sets. We then report on such an implementation of grounding completely on first-order theories rather than on programs (i.e., as is the case with traditional ASP solvers), and show that the new approach is quite competitive with current effective solvers on very large instances of the Hamiltonian circuit program. In addition, we further consider the translation of logic programs with aggregates (a very important building block of ASP) under the stable model semantics, into classical first-order theories. Preferences play an important role in knowledge representation and reasoning. In the past decade, a number of approaches for handling preferences have been developed in various nonmonotonic reasoning formalisms, while adding preferences into ASP has been known to have promising advantages from both implementation and application viewpoints. This thesis also extends the notion of preferred ASP (i.e., answer set programming with preferrence relations among the rules), that is currently only formalized for propositional programs, into the notion of first-order ASP. To this aim, we develop both a (first-order) fixpoint type characterization that is similar to Zhang and Zhou's progression semantics, and a classical logic formulation so that the preferred answer sets are exactly those models of the logic formula. We further show that the fixpoint type characterization and classical logic formulation coincide.

Date of Award	2013
Original language	English