Formalizing nonmonotonic reasoning systems (Q1099647)

The paper addresses the problem of existence of expansions of semi-normal default theories introduced by \textit{R. Reiter} [ibid. 13, 81-132 (1980; Zbl 0435.68069)]. Semi-normal default theory \(\Delta\) is defined as (D,W), where W is a set of first-order formulae, and D is a set of semi- normal defaults, i.e. rules of inference having the form: (*)\ \(\frac{\alpha,M(\beta \wedge \gamma)}{\beta}\), where \(\alpha\), \(\beta\), and \(\gamma\) are first-order formulae, and M is the possibility operator. Extension of semi-normal default theory \(\Delta\) is defined as a minimal set E satisfying the following system of recursive equations: \(E_ 0=W\quad E_{i+1}=Cn(E_ i)\cup \{\beta|\frac{\alpha,M(\beta \wedge \gamma)}{\beta}\in D\) \& \(\alpha \in E_ i\) \& \(\neg (\beta \wedge \gamma)\not\in E_ i\}\quad E=\cup^{\infty}_{i=0}E_ i,\) where Cn(X) is the set of all first-order consequences of X. Extensions play the role of models for default theories hence the importance of the problem of their existence. The author defines a subclass of ordered quantifier-free semi-normal default theories (let us call it \({\mathcal O}rd)\), and proves that every of its element has at least one extension. Moreover the author presents a non-deterministic procedure, which is guaranteed to find such extension for (D,W)\(\in {\mathcal O}rd\), provided that both D and W are finite, \(\alpha\) and \(\beta\) in (*) are literals (atomic or negated atomic formulae), and \(\gamma\) in (*) is a (possibly empty) conjunction of literals. This procedure - according to author's reference to his M.Sc. Thesis - forms a non-deterministic decision procedure for the problem: ``Is Cn(H) an extension of \(\Delta\) ?'' for certain finite (not necessarily semi-normal) single-justification default theories \(\Delta\) and finite H, and therefore may serve as a reliable basis for a variety of other reasoning procedures. The procedure, however, needs an oracle for the relation \(\nvdash\) of first-order non-provability. The author shows how through a pertinent formalization one can translate inheritance networks with exceptions into \({\mathcal O}rd.\) The last part of the paper contains a comparison of the proposed approach with others applicable to semantic networks and truth maintenance systems, which are known to possess tractable reasoning procedures. Some methodological issues are discussed there. Errors in strategic points of the paper may be misleading for the reader. Exclusion of existential quantifiers is implicit. On page 44, \(line_{5,4}\), the author misquotes the Reiter's definition of extension: according to author's version Cn(\(\neg A)\) is an extension of \(\Delta =(\{\frac{MA}{\neg A}\},0)\), while it is not in light of Reiter's theorem the author quotes (with erroneous clause ``and for \(i>0'')\) on page 67. Also an informal interpretation of extension, page 45, \(line_{17\div 14}\), is faulty (pose \(D=0\), \(W=\{A\equiv B\}\), \(E=Cn(\{A\equiv B,A,B\})\), as counterexample). In the main definition of relation \(\ll\) on page 49, besides of other errors, a requirement that \(\ll\) is the least relation satisfying the imposed conditions is missing. Most of concrete examples discussed in the paper are not in \({\mathcal O}rd\), even such unproblematic default theory like (\(\{\frac{M(A\wedge \neg B)}{A}\), \(\frac{M(B\wedge \neg A)}{B}\},0)\), therefore it is rather difficult to fully appreciate the author's approach. It should be noted, however, that \({\mathcal O}rd\) is closed under \(\subseteq\). Taking into account, that there exist semi-normal theories \(\Delta\),\(\Delta\) ' such that \(\Delta\subseteq \Delta '\), and \(\Delta\) has no extensions, while \(\Delta\) ' has one, \({\mathcal O}rd\) seems to be a serious restriction of the class of all semi-normal default theories.