Linear resolution for consequence finding
type: Item
instance of: scholarly article
title: Linear resolution for consequence finding
zbMATH Open document ID: 0805.68105
DOI: 10.1016/0004-3702(92)90030-2
author: Katsumi Inoue
published in: Artificial Intelligence
publication date: 1993-01-17T00:00:00Z
review text: 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 meth…
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 68T30
zbMATH DE Number: 96250
zbMATH Keywords: resolution
zbMATH Keywords: SOL-resolution
zbMATH Keywords: consequence-finding
zbMATH Keywords: production field
zbMATH Keywords: model elimination
MaRDI profile type: Publication
full work available at URL: 0004-3702(92)90030-2
OpenAlex ID: W1965184317
cites work: Saturation, nonmonotonic reasoning and the closed-world assumption
cites work: Q5679729
cites work: Q3786007
cites work: Q3489523
cites work: Q4012181
cites work: On the relationship between circumscription and negation as failure
cites work: A circumscriptive theorem prover
cites work: Q4012237
cites work: Q4012182
cites work: An incremental method for generating prime implicants/implicates
cites work: Q5621960
cites work: Linear resolution with selection function
cites work: Q3198885
cites work: Q3339245
cites work: A Simplified Format for the Model Elimination Theorem-Proving Procedure
cites work: Q4139711
cites work: Circumscription - a form of non-monotonic reasoning
cites work: A note on linear resolution strategies in consequence-finding
cites work: A fixpoint semantics for disjunctive logic programs
cites work: A logical framework for default reasoning
cites work: Compiling a default reasoning system into Prolog
cites work: An algorithm to compute circumscription
cites work: The Problem of Simplifying Truth Functions
cites work: Two Results on Ordering for Resolution with Merging and Linear Format
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Refutation graphs
cites work: A Prolog technology theorem prover: Implementation by an extended Prolog compiler
cites work: Natural language and logic. International scientific symposium, Hamburg, FRG, 9-11 May 1989. Proceedings
cites work: RST Flip-Flop Input Equations
cites work: Q3795647
description: scientific article; zbMATH DE number 96250