First-Order Stable Model Semantics and First-Order Loop Formulas
This work addresses a theoretical gap in logic programming by extending loop formulas to first-order cases, enabling more efficient reasoning for researchers in knowledge representation and AI.
The paper investigates the relationship between first-order stable model semantics and first-order loop formulas, extending loop formulas to disjunctive programs and arbitrary first-order theories, and introduces a syntax extension with explicit quantifiers for reasoning with non-Herbrand stable models using first-order reasoners.
Lin and Zhaos theorem on loop formulas states that in the propositional case the stable model semantics of a logic program can be completely characterized by propositional loop formulas, but this result does not fully carry over to the first-order case. We investigate the precise relationship between the first-order stable model semantics and first-order loop formulas, and study conditions under which the former can be represented by the latter. In order to facilitate the comparison, we extend the definition of a first-order loop formula which was limited to a nondisjunctive program, to a disjunctive program and to an arbitrary first-order theory. Based on the studied relationship we extend the syntax of a logic program with explicit quantifiers, which allows us to do reasoning involving non-Herbrand stable models using first-order reasoners. Such programs can be viewed as a special class of first-order theories under the stable model semantics, which yields more succinct loop formulas than the general language due to their restricted syntax.