The Resolution Calculus

The Resolution Calculus

by Alexander Leitsch

Paperback(Softcover reprint of the original 1st ed. 1997)

View All Available Formats & Editions
Use Standard Shipping. For guaranteed delivery by December 24, use Express or Expedited Shipping.

Product Details

ISBN-13: 9783642644733
Publisher: Springer Berlin Heidelberg
Publication date: 09/28/2011
Series: Texts in Theoretical Computer Science. An EATCS Series
Edition description: Softcover reprint of the original 1st ed. 1997
Pages: 300
Product dimensions: 6.10(w) x 9.25(h) x 0.03(d)

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.- 2.4.1 Gilmore’s Method.- 2.4.2 The Method of Davis and Putnam.- 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.

Customer Reviews

Most Helpful Customer Reviews

See All Customer Reviews