Ordered completion for first-order logic programs on finite structures

• Published in: Artificial intelligence 2012-02, Vol.177, p.1-24
• Main Authors: Asuncion, Vernon, Lin, Fangzhen, Zhang, Yan, Zhou, Yi
• Format: Article
• Language: English
• Subjects: Answer set programming; Applied sciences; Artificial intelligence; Computer science; control theory; systems; Derivation; Exact sciences and technology; Expert systems; Knowledge representation; Learning and adaptive systems; Logic programming; Logical, boolean and switching functions; Mathematical analysis; Nonmonotonic reasoning; Ordered completion; Semantics; Sentences; Solvers; Theoretical computing; Translations
• ISSN: 0004-3702; 1872-7921
• DOI: 10.1016/j.artint.2011.11.001

In this paper, we propose a translation from normal first-order logic programs under the stable model semantics to first-order sentences on finite structures. The translation is done through, what we call, ordered completion which is a modification of Clarkʼs completion with some auxiliary predicates added to keep track of the derivation order. We show that, on finite structures, classical models of the ordered completion of a normal logic program correspond exactly to the stable models of the program. We also extend this result to normal programs with constraints and choice rules. From a theoretical viewpoint, this work clarifies the relationships between normal logic programming under the stable model semantics and classical first-order logic. It follows that, on finite structures, every normal program can be defined by a first-order sentence if new predicates are allowed. This is a tight result as not every normal logic program can be defined by a first-order sentence if no extra predicates are allowed or when infinite structures are considered. Furthermore, we show that the result cannot be extended to disjunctive logic programs, assuming that NP ≠ coNP . From a practical viewpoint, this work leads to a new type of ASP solver by grounding on a programʼs ordered completion instead of the program itself. We report on a first implementation of such a solver based on several optimization techniques. Our experimental results show that our solver compares favorably to other major ASP solvers on the Hamiltonian Circuit program, especially on large domains.