Saturation, nonmonotonic reasoning and the closed-world assumption (Q1060864)

The problem of drawing negative conclusions of information contained in a data base, with some version of the so called ''closed world assumption'' (abbr: cwa), is investigated in this paper. In the sense of \textit{R. Reiter} [Logic and Data Bases, 55-76 (1978; Zbl 0412.68089)] cwa has the following interpretation (abbr: \(cwa_ R)\). The data base is represented by a set of elementary sentences true in a certain world. For the purpose of minimizing the data base, only positive sentences explicitly appear in it, whereas the negative ones are assumed to be true whenever they do not contradict the data base itself. In other words, \(cwa_ R\) is an assumption of the completeness of the data base with respect to positive elementary sentences. The reasoning based on it has not, in general, the property of monotonicity, i.e., an update of the data base may cause the falsification of some of its previous consequences. E.g., \(\neg q\) may be inferred from \(cwa_ R+\{p\}\), but not from \(cwa_ R+\{p,q\}\). Many authors modify the above interpretation of cwa by including some true but nonelementary sentences in the data base. In this case the assumption of the completeness may lead to a contradiction. E.g., if p and q are positive elementary sentences then both \(\neg p\) and \(\neg q\), that is, \(\neg (p\vee q)\) follows from \(cwa_ R+\{p\vee q\}.\) This paper contains a proposition of non-monotonic reasoning based on some generalization of \(cwa_ R\) in a way which avoids such a paradox (other, also non-monotonic solutions of the slightly more general problem of making information more complete can be found in papers by \textit{D. McDermott} and \textit{J. Doyle} [Artif. Intell. 13, 41-72 (1980; Zbl 0435.68074)] and \textit{R. Reiter} [ibid. 13, 81-132 (1980; Zbl 0435.68069)]). This proposition is a semantical analogon of the syntactic notion of ''predicate circumscription'' of \textit{J. McCarthy} [ibid. 13, 27- 39 (1980; Zbl 0435.68073)]. In this paper the following definitions have been introduced, which we quote according to the notation of the Handbook of Mathematical Logic. In particular L denotes (a certain fixed) first-order language without the equality symbol, \({\mathfrak M},{\mathfrak N},..\). are structures for L,M,N,... their universes, P,Q,... are sets of sentences of L, and p,q,... formulae of L. The relation \(\prec\), equivalent to the relation \(\preccurlyeq\) of \textit{W. Lipski jun.} [Lect. Notes Comput. Sci. 53, 374-381 (1977; Zbl 0363.02025)], is defined as: \({\mathfrak M}\prec {\mathfrak N}\) iff \(M=N\) and for each function symbol f of L, \(f^{{\mathfrak M}}=f^{{\mathfrak N}}\), and for each relation symbol r of L, \(r^{{\mathfrak M}}\subseteq r^{{\mathfrak N}}\). Class \({\mathcal K}\) of the structures for L is said to be closed iff with every element of \({\mathcal K}\) its \(\prec\)-predecessor is a member of \({\mathcal K}\). Recall that a subclass \({\mathcal F}\) of a class \({\mathcal K}\) is said to be dense (relative to \(\prec)\) in \({\mathcal K}\) iff for each \({\mathfrak M}\in {\mathcal K}\) there exists \({\mathfrak N}\in {\mathcal F}\) such that \({\mathfrak N}\prec {\mathfrak M}\) (in the paper the term ''minors'' is used instead of ''is dense in''). A structure \({\mathfrak M}\) is said to be discriminant iff for each pair of constant and nonidentical terms (t,u) of L, \(t^{{\mathfrak M}}\neq u^{{\mathfrak M}}\). The class of all discriminant models of P is denoted by dis[P]. P is said to be minimally modelable iff the class of all minimal (relative to \(\prec)\) models of P is dense in the class of all models of P. The relation \(\Vdash\) of sub-implication between sets of sentences and sentences or sets of sentences of L, the key notion of the paper, has been definded as: \(P\Vdash Q\) iff there exists in dis[P] a closed and dense sub-class of models of Q. The relation \(\Vdash\) is non-monotonic. In particular, if r is a 0-ary relation symbol of L then \(0\Vdash\neg r\), but \(\{\) \(r\}\) non \(\Vdash \neg r.\) In this paper atomic and negated atomic sentences are taken as elementary. A positive sentence is defined as any sentence logically equivalent to a formula composed of, at most, the following connectives: \(\forall\), \(\exists\), \(\vee\) and \(\wedge\). The data base is a set of sentences of L, and is usually denoted by P. The notion of cwa appears in the paper, with the exception of the title, only once and in a quite irrelevant context. However, one can suppose, that its following interpretation has been adopted: \(cwa_{BS} \equiv\) all models are discriminant and minimal relative to \(\prec\), which is justified by Property 1.6.3: if P is minimally modelable then \(P\Vdash Q\) is equivalent to \((cwa_{BS}+P)\vDash Q.\) Some properties of the relation \(\Vdash\) are proved in the paper. If Q is a set of positive sentences then \(P\Vdash Q\) is equivalent to \(P\vDash Q\). \(P\Vdash p\wedge q\) is equivalent to the conjunction of \(P\Vdash p\) and \(P\Vdash q\). If \(P\Vdash q\) then P non \(\Vdash \neg q\). (Perhaps for every set P of atomic sentences and every atomic sentence q of L, \(P\Vdash \neg q\) is equivalent to \(q\not\in P\), which would give the evidence that \(cwa_{BS}\) is a generalization of \(cwa_ R.)\) Moreover, it has been proved that in some particular cases \(\forall\)-theory is minimally modelable. A large part of the paper concerns a case in which P is a set of ''groundable clauses, defined as generalizations of formulae p of the form \(p_ 1\vee...\vee p_ n\), where each \(p_ i\) is an atomic or negated atomic formula, none of \(p_ i\) contains a function symbol (other than a constant symbol), and each variable, which appears in p, appears also in some negated atomic formula \(p_ i.In\) this particular case, which implies minimal modelability and then the mentioned interpretation \(cwa_{BS}\), a decision algorithm for \(P\Vdash q\) has been constructed by the resolution method. The algorithm works if P is finite and q is a so called ''g-formula'' (definition 3.1.1). The paper seems to be overcomplicated. Certain observations have been supplied with long and, so to speak, sophisticated proofs. Example. Each \(\forall\)-theory is minimally modelable. Proof. Let \({\mathcal K}\) be a chain (relative to \(\prec)\) of models of an \(\forall\)-theory P. Let \({\mathfrak M}=\cap {\mathcal K}\). It may be easily checked by induction, that for every quantifier-free formula q and assignment s in \({\mathfrak M}\), if \({\mathfrak N}\vDash q[s]\) for all \({\mathfrak N}\in {\mathcal K}\) then \({\mathfrak M}\vDash q[s]\). Thus (\(\forall {\mathfrak N}\in {\mathcal K})\) (\({\mathfrak N}\vDash \forall xq)\) implies \({\mathfrak M}\vDash \forall xq\), and hence \({\mathfrak M}\vDash P\). By the Kuratowski-Zorn Lemma we obtain the thesis. A slightly weaker version of this theorem (Property 1.3.2) takes two and a half pages of informal proof in the paper. Also, the second proof with respect to length (one and a half pages) of Property 3.2.1 may be analogically reduced to a few lines of print.