nach oben

1997 | Buch

Kapitel lesen Erstes Kapitel lesen

The Resolution Calculus

verfasst von: Prof.Dr. Alexander Leitsch

Verlag: Springer Berlin Heidelberg

Buchreihe : Texts in Theoretical Computer Science. An EATCS Series

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten

Über dieses Buch

The History of the Book In August 1992 the author had the opportunity to give a course on resolution theorem proving at the Summer School for Logic, Language, and Information in Essex. The challenge of this course (a total of five two-hour lectures) con sisted in the selection of the topics to be presented. Clearly the first selection has already been made by calling the course "resolution theorem proving" instead of "automated deduction" . In the latter discipline a remarkable body of knowledge has been created during the last 35 years, which hardly can be presented exhaustively, deeply and uniformly at the same time. In this situ ation one has to make a choice between a survey and a detailed presentation with a more limited scope. The author decided for the second alternative, but does not suggest that the other is less valuable. Today resolution is only one among several calculi in computational logic and automated reasoning. How ever, this does not imply that resolution is no longer up to date or its potential exhausted. Indeed the loss of the "monopoly" is compensated by new appli cations and new points of view. It was the purpose of the course mentioned above to present such new developments of resolution theory. Thus besides the traditional topics of completeness of refinements and redundancy, aspects of termination (resolution decision procedures) and of complexity are treated on an equal basis.

Inhaltsverzeichnis

Frontmatter

1. Introduction

Abstract

Logic calculi can serve for many purposes, such as reconstructing and analyzing mathematical proofs in a formal manner or automating the search for mathematical proofs. As the paradoxes of set theory struck the mathematical community around 1900, the formal and consistent representation of theories became a central issue in foundational research. In the theory of proofs fascinating results were obtained in the 1930s, which culminated in the completeness and incompleteness (or better “incompletability”) results of Godel [Göd30],[Göd31]. Somewhat later Gentzen defined a natural notion of formal proofs [Gen34], which is closer to actual mathematical deduction than the so-called Hilbert-type systems. Like Herbrand [Her30] Gentzen investigated the form and structure of mathematical proofs, while Gödel’s famous theorems were more directed to provability.

Alexander Leitsch

2. The Basis of the Resolution Calculus

Abstract

Throughout the whole book we will focus on theorem proving in the context of first-order logic. First-order logic plays an important role in mathematical logic and computer science. First of all it is a rich language, by which algebraic theories, computational problems, and substantial knowledge representation in Artificial Intelligence can be expressed; due to its ability to represent undecidable problems (like the halting problem for Turing machines) first-order logic (or more precisely, the validity problem for first-order logic) is undecidable. On the other hand, the valid formulas of first-order logic can be obtained by logical calculi and thus are recursively enumerable. In this sense, first-order logic is mechanizable (we can find a proof for every valid sentence, but there is no decision procedure for validity).

Alexander Leitsch

3. Refinements of Resolution

Abstract

In Chapter 2 we have proved the correctness and completeness of the resolution principle. It might seem that these are already the key results of resolution theory. Although the (general) resolution principle is clearly superior to the PR-deduction principle and to methods based on Herbrand’s theorem, there are several reasons for further refining the deduction principle. First of all the high number of resolvents derivable from a set of clauses is a serious obstacle to practical applications. Thus it is significant that Robinson presented a paper on hyperresolution [Rob65a], a refinement to be described later, in the same year as his landmark paper on resolution [Rob65] was published. So one motivation for restricting the R-deduction principle is efficiency.

Alexander Leitsch

4. Redundancy and Deletion

Abstract

The problems of showing the existence of proofs and finding proofs of given theorems mark the borderline between mathematical logic and computer science. So far we merely proved results about the existence of refutations for unsatisfiable sets of clauses under various types of refinements; we have not spoken about how to (really) obtain refutations. In our formalism the situation can be described in the following way: Let Ψ be an arbitrary complete refinement and C be an unsatisfiable set of clauses. By the completeness of Ψ there exists a refutation Γ ∈ Ψ(∁); finding such a Γ (within reasonable computing time) is the main problem of automated deduction. At this point we face the problem of search which is of central importance to all fields of Artificial Intelligence. With regard to a resolution refinement, search is an algorithmic method for producing the elements of Ψ(∁) until a refutation is found (in principle we can try to find all Ψ-refutations of ∁, but such a procedure usually is nonterminating). The computational cost of proof search is, in practice, the main obstruction to automated theorem proving. For this reason, several techniques have been invented to reduce search. We list three of them:

Alexander Leitsch

5. Resolution as Decision Procedure

Abstract

In Section 2.7 we showed that for every unsatisfiable set of clauses there exists a resolution refutation. In the last two chapters we have exhibited some completeness preserving extensions of resolution. Here we will focus on another aspect of refinements, namely termination. Suppose that we start a theorem prover (i.e., a complete resolution refinementR_x) on a set of clauses ∁, which may be satisfiable or unsatisfiable. Obviously there are three possibilities:

R_x terminates on ∁ and refutes ∁. Because R_x is correct and □ ∈ R_x(∁) we know that ∁ is unsatisfiable.

R_x terminates on ∁ without producing □.By the completeness of R_x ∁ must be satisfiable.

R_x does not terminate on ∁: In this case R_x(∁) is infinite and □ ∉ R_x (∁) (we assume that the production of new clauses is stopped as soon as □ is derived). As in case 2) ∁ is satisfiable, but we cannot detect this property just by computing R_x(∁).

Alexander Leitch

6. On the Complexity of Resolution

Abstract

By the undecidability of clause logic there exists no recursive bound on the length of refutations of clause sets ∁ in terms of the length of ∁, regardless of what logic calculus and what concept of length are chosen. Thus we cannot present a complexity theory similar to that of propositional inference systems [Boe92], Instead there are basically two different mathematical approaches to proof complexity in predicate logic:

Analyze the relative complexity of resolution versus other inference methods.

Define some absolute complexity measure for sets of clauses which is independent of deduction concepts but is recursively related to all “reasonable” inference systems.

Alexander Leitsch

Backmatter

Titel: The Resolution Calculus
verfasst von: Prof.Dr. Alexander Leitsch
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-60605-2
Print ISBN: 978-3-642-64473-3
DOI: https://doi.org/10.1007/978-3-642-60605-2

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

1. Introduction

2. The Basis of the Resolution Calculus

3. Refinements of Resolution

4. Redundancy and Deletion

5. Resolution as Decision Procedure

6. On the Complexity of Resolution

Backmatter