In this paper, we extend the progression semantics for first-order disjunctive logic programs and show that it coincides with the stable model semantics. Based on it, we further show how disjunctive answer set programming is related to Satisfiability Modulo Theories.

In this paper, we propose a translation from normal first-order logic programs under the answer set semantics to first-order theories on finite structures. Specifically, we introduce ordered completions which are modifications of Clark's completions with some extra predicates added to keep track of the derivation order, and show that on finite structures, classical models of the ordered-completion of a normal logic program correspond exactly to the answer sets (stable models) of the logic program.

In this paper, we propose a progression semantics for first-order answer set programs. Based on this new semantics, we are able to define the notion of boundedness for answer set programming. We prove that boundedness coincides with the notions of recursion-free and loop-free under program equivalence, and is also equivalent to first-order definability of answer set programs on arbitrary structures.