The Resolution Calculus
This is a completely new presentation of resolution as a logical calculus and as a basis for computational algorithms and decision procedures. The first part deals with the traditional topics (Herbrand's theorem, completeness of resolution, refinements and deletion) but with many new features a...
| Main Author: | |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
1997, 1997
|
| Edition: | 1st ed. 1997 |
| Series: | Texts in Theoretical Computer Science. An EATCS Series
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- The Basis of the Resolution Calculus
- First-Order Logic
- Transformation to Clause Form
- Term Models and Herbrand’s Theorem
- Decision Methods for Sets of Ground Clauses
- The Propositional Resolution Principle
- Substitution and Unification
- The General Resolution Principle
- A Comparison of Different Resolution Concepts
- 3. Refinements of Resolution
- A Formal Concept of Refinement
- Normalization of Clauses
- Refinements Based on Atom Orderings
- Lock Resolution
- Linear Refinements
- Hyperresolution
- Refinements: A Short Overview
- 4. Redundancy and Deletion
- The Problem of Proof Search
- The Subsumption Principle
- Subsumption Algorithms
- The Elimination of Tautologies
- Clause Implication
- 5. Resolution as Decision Procedure
- The Decision Problem
- A-Ordering Refinements as Decision Procedures
- Hyperresolution as Decision Procedure
- Hyperresolution and Automated Model Building
- 6. On the Complexity of Resolution
- Herbrand Complexity and Proof Length
- Extension and the Use of Lemmas
- Structural Normalization
- Functional Extension