Stable models and circumscription
type: Item
instance of: scholarly article
title: Stable models and circumscription
zbMATH Open document ID: 1227.68103
author: Paolo Ferraris
author: Joohyung Lee
author: Vladimir Lifschitz
published in: Artificial Intelligence
publication date: 2011-06-17T00:00:00Z
review text: Consider the logical symbols \(\vee, \wedge, \neg, \rightarrow, \forall, \exists\). Let \(\mathbf{p}\) be a list of distinct predicate constants \({p}_{1},\ldots,p_{n}\). For any first-order formula \({F}\), let \(SM_{\mathbf{p}}\)[\({F}\)] denote the second-order formula \({F} \wedge \neg \exists \mathbf{u} ((\mathbf{u} < \mathbf{p} \wedge {F} ^{*} (\mathbf{u}))\), where \(\mathbf{u}\) is a list of \({n}\) distinct predicate variables \({u}_{1},\ldots,u_{n}\), and \({F} ^{*} (\mathbf{u})\) is defined recursively: \({p}_{i} (\mathbf{t}) ^{*}\) = \({p}_{i} (\mathbf{t})\) for any tuple \(\mathbf{t}\) of terms; \({F} ^{*}\) = \({F}\) for any atomic formula \({F}\) that does not contain members of \(\mathbf{p}\); \(({F} \wedge {G})^{*}\) = \({F}^{*} \wedge {G}^{*}\); \(({F} \vee {G})^{*}\) = \({F}^{*} \vee {G}^{*}\); \(({F} \rightarrow {G})^{*}\) = \(({F}^{*} \rightarrow {G}^{*}) \wedge ({F} \rightarrow {G})\); \((\forall {xF})^{*}\) = \(\forall {xF}^{*}\); \((\exists {xF})^{*}\) = \(\exists { xF}^{*}\). For any sentence \({F}\), a \(\mathbf{p}\)-stable model of \(F\) is an interpretation of the underlying signature that satisfies \(SM_{\mathbf{p}}\)[\({F}\)]. The proposed stable model is applicable to syntactically complex formulas because it covers non-Herbrand models and because it allows to distinguish between intensional and extensional predicates. Syntactically complex formulas are useful in the context of the stable model semantics in view of their relation to aggregates. Non-Herbrand models are related to the use of arithmetic functions in logic programs. Extensional predicates provide a useful technical device. The concept of a stable model provides a declarative semantics for Prolog programs with negation as failure and can become a starting point for development of answer set programming.
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 68N17
zbMATH DE Number: 5909442
zbMATH Keywords: answer set programming
zbMATH Keywords: circumscription
zbMATH Keywords: nonmonotonic reasoning
zbMATH Keywords: program complition
zbMATH Keywords: stable models
describes a project that uses: ASSAT
MaRDI profile type: Publication
full work available at URL: j.artint.2010.04.011
OpenAlex ID: W2134039900
cites work: Tight logic programs
cites work: Q3007261
cites work: Logic Programming and Nonmonotonic Reasoning
cites work: Q3983043
cites work: Loop formulas for circumscription
cites work: Q3112629
cites work: Safe Formulas in the General Theory of Stable Models (Preliminary Report)
cites work: Strongly equivalent logic programs
cites work: A Characterization of Strong Equivalence for Logic Programs with Variables
cites work: Twelve Definitions of a Stable Model
cites work: Rules as actions: A situation calculus semantics for logic programs
cites work: A logic of knowledge and justified assumption
cites work: ASSAT: computing answer sets of a logic program by SAT solvers
cites work: From answer set logic programming to circumscription via logic of GK
cites work: Q4702577
cites work: Circumscription - a form of non-monotonic reasoning
cites work: Semantical considerations on nonmonotonic logic
cites work: Logic programs with stable model semantics as a constraint programming paradigm
cites work: Achieving compositionality of the stable model semantics for <scp>smodels</scp> programs
cites work: Q4736482
cites work: A logic for default reasoning
cites work: Extending and implementing the stable model semantics
cites work: Tight, consistent, and computable completions for unrestricted logic programs
DOI: 10.1016/J.ARTINT.2010.04.011
description: scientific article; zbMATH DE number 5909442