Sinossi
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.
Le informazioni nella sezione "Riassunto" possono far riferimento a edizioni diverse di questo titolo.
