Stable models and circumscription (Q543596): Difference between revisions
From MaRDI portal
Changed an Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 07:57, 30 January 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Stable models and circumscription |
scientific article |
Statements
Stable models and circumscription (English)
0 references
17 June 2011
0 references
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.
0 references
answer set programming
0 references
circumscription
0 references
nonmonotonic reasoning
0 references
program complition
0 references
stable models
0 references