A generalization of the Lin-Zhao theorem

Paolo Ferraris, Joohyung Lee, Vladimir Lifschitz

Research output: Contribution to journalArticle

34 Citations (Scopus)

Abstract

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 language English (US) 79-101 23 Annals of Mathematics and Artificial Intelligence 47 1-2 https://doi.org/10.1007/s10472-006-9025-2 Published - Jun 2006

Theorem
Stable Models
Logic Programs
Simplification
Completion
Simplify
Generalization
Cover
Generalise

Keywords

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

ASJC Scopus subject areas

• Artificial Intelligence
• Applied Mathematics

Cite this

A generalization of the Lin-Zhao theorem. / Ferraris, Paolo; Lee, Joohyung; Lifschitz, Vladimir.

In: Annals of Mathematics and Artificial Intelligence, Vol. 47, No. 1-2, 06.2006, p. 79-101.

Research output: Contribution to journalArticle

Ferraris, Paolo ; Lee, Joohyung ; Lifschitz, Vladimir. / A generalization of the Lin-Zhao theorem. In: Annals of Mathematics and Artificial Intelligence. 2006 ; Vol. 47, No. 1-2. pp. 79-101.
@article{374f20c6666d48b297cf4622d284f428,
title = "A generalization of the Lin-Zhao theorem",
abstract = "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.",
keywords = "Answer set programming, Clark's completion, Logic programming, Loop formulas, Nonmonotonic reasoning, Stable models",
author = "Paolo Ferraris and Joohyung Lee and Vladimir Lifschitz",
year = "2006",
month = "6",
doi = "10.1007/s10472-006-9025-2",
language = "English (US)",
volume = "47",
pages = "79--101",
journal = "Annals of Mathematics and Artificial Intelligence",
issn = "1012-2443",
publisher = "Springer Netherlands",
number = "1-2",

}

TY - JOUR

T1 - A generalization of the Lin-Zhao theorem

AU - Ferraris, Paolo

AU - Lee, Joohyung

AU - Lifschitz, Vladimir

PY - 2006/6

Y1 - 2006/6

N2 - 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.

AB - 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.

KW - Answer set programming

KW - Clark's completion

KW - Logic programming

KW - Loop formulas

KW - Nonmonotonic reasoning

KW - Stable models

UR - http://www.scopus.com/inward/record.url?scp=33750972879&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33750972879&partnerID=8YFLogxK

U2 - 10.1007/s10472-006-9025-2

DO - 10.1007/s10472-006-9025-2

M3 - Article

VL - 47

SP - 79

EP - 101

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

SN - 1012-2443

IS - 1-2

ER -