Stable models and circumscription (Q543596)

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.