Ordered completion for first-order logic programs on finite structures

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.