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 book deals with the traditional topics in new ways and gives a systematic treatment of recent research topics. It should become a standard reference.

Inhalt
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.