First-order stable model semantics and first-order loop formulas

Joohyung Lee, Yunsong Meng

Research output: Contribution to journalArticlepeer-review

14 Scopus citations


Lin and Zhao's 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.

Original languageEnglish (US)
Pages (from-to)125-180
Number of pages56
JournalJournal of Artificial Intelligence Research
StatePublished - Sep 2011

ASJC Scopus subject areas

  • Artificial Intelligence


Dive into the research topics of 'First-order stable model semantics and first-order loop formulas'. Together they form a unique fingerprint.

Cite this