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.