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

arXiv: https://arxiv.org/abs/1401.3898 · HTML: https://mlsanity.com/paper/1401.3898/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Jan 2014.

## Built on by (most cited first, 3 of 3)

- [Verification of Locally Tight Programs](https://mlsanity.com/paper/2204.10789/) (2022)
- [Weighted Rules under the Stable Model Semantics](https://mlsanity.com/paper/2605.09519/) (2026)
- [Relating Answer Set Programming and Many-sorted Logics for Formal Verification](https://mlsanity.com/paper/2502.09230/) (2025)

## Abstract (arXiv)

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.