Linear resolution for consequence finding (Q1199916)

Resolution is mostly used as refutational method. However, it is an old result of \textit{R. C. T. Lee} [``A completeness theorem and computer program for finding theorems derivable from given axioms'', Ph. D. Thesis, Univ. California, Berkeley, CA (1967)] that resolution is also complete for consequence finding (if \(C\) is a non-tautological clause implied by a set of clauses \(\mathcal C\) then there exist a clause \(D\) such that \(D\) is derivable from \(\mathcal C\) and \(D\) subsumes \(C\)). The author of this paper uses SOL-resolution, an adapted version of model elimination, as a consequence-finding method. For the description of the problem of consequence-finding, the author develops an abstract framework around the central concept of production field. In a production field a specific subset of literals is specified of which the consequence clauses must consists (plus further syntax restrictions). The set of theorems derivable from a set of clauses which belong to a production field and are closed under subsumption form the so-called set of characteristic clauses (one of the key notions of this paper). The author gives several applications in the area of AI (abductive reasoning, prime implicates, truth maintenance systems and circumscription), where his general terminology leads to a unified and systematic treatment. The concept of SOL-resolution defined in this paper (skipping ordered linear \(r\)) is a method for consequence-finding which is close to model elimination and generalizes several other consequence- finding methods used so far [see, e.g., \textit{T. C. Przymusiński}, Artif. Intell. 38, No. 1, 49-73 (1989; Zbl 0663.68098)]. The operation of skipping is characteristic to consequence-finding (it selects a specific group of literals and ``protects'' them from resolution cut). It is pointed out that the techniques of reduction and resolution (as defined in the model elimination method) must be used nondeterministically and that some preference methods used in the standard literature (such as OL- resolution) are incomplete. Eventually, it is proved that SOL-resolution is sound and complete for consequence-finding. By the general, mathematically rigorous terminology and by the completeness result for an efficient (predicate logic) method of consequence-finding, the paper is an important contribution to AI-logic and automatic deduction. Some minor details only: Even in the case of propositional logic, ``\(C\) subsumes \(D\)'' is not equivalent to the validity of \(C\to D\) (this holds only if \(D\) is not a tautology); the restriction to nontautological clauses is also important to the validity of Lee's theorem.