First-Order Stable Model Semantics and First-Order Loop Formulas

TL;DR

This paper explores the relationship between first-order stable model semantics and loop formulas, extending definitions and syntax to enable reasoning with non-Herbrand stable models using first-order logic.

Contribution

It extends the concept of first-order loop formulas to disjunctive programs and arbitrary theories, and introduces explicit quantifiers for reasoning with non-Herbrand models.

Findings

Extended loop formulas to disjunctive and arbitrary first-order theories

Developed syntax with explicit quantifiers for stable model reasoning

Facilitated reasoning with non-Herbrand stable models using first-order reasoners

Abstract

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.