A generalization of the Lin-Zhao theorem

Paolo Ferraris, Joohyung Lee, Vladimir Lifschitz

Research output: Contribution to journalArticlepeer-review

37 Scopus citations


The theorem on loop formulas due to Fangzhen Lin and Yuting Zhao shows how to turn a logic program into a propositional formula that describes the program's stable models. In this paper we simplify and generalize the statement of this theorem. The simplification is achieved by modifying the definition of a loop in such a way that a program is turned into the corresponding propositional formula by adding loop formulas directly to the conjunction of its rules, without the intermediate step of forming the program's completion. The generalization makes the idea of a loop formula applicable to stable models in the sense of a very general definition that covers disjunctive programs, programs with nested expressions, and more.

Original languageEnglish (US)
Pages (from-to)79-101
Number of pages23
JournalAnnals of Mathematics and Artificial Intelligence
Issue number1-2
StatePublished - Jun 2006


  • Answer set programming
  • Clark's completion
  • Logic programming
  • Loop formulas
  • Nonmonotonic reasoning
  • Stable models

ASJC Scopus subject areas

  • Artificial Intelligence
  • Applied Mathematics


Dive into the research topics of 'A generalization of the Lin-Zhao theorem'. Together they form a unique fingerprint.

Cite this