Front Cover; Automated Theorem Proving: A Logical Basis; Copyright Page; Dedication; PREFACE; Table of Contents; ACKNOWLEDGEMENTS; CHAPTER 1. THE ROLE OF LOGICAL SYSTEMS; 1.1. Orientation; 1.2. The basic concepts of first-order logic; 1.3. The formal presentation of problems; 1.4. Refutation procedures; 1.5. Preparation of formulas; 1.6. The Herbrand Theorem; 1.7. Summary; CHAPTER 2. BASIC RESOLUTION; 2.1. Introduction; 2.2. The Davis-Putnam Procedure; 2.3. Ground resolution; 2.4. Semantic Trees; 2.5. General resolution: Unification; 2.6. The general resolution procedure; 2.7. Summary

CHAPTER 3. REFINEMENTS OF RESOLUTION3.1. Introduction; 3.2. Unit preference and set-of-support; 3.3. Ordered clause deductions; 3.4. Setting refinements; 3.5. Linear refinements; 3.6. Model elimination; 3.7. Summary; CHAPTER 4. SUBSUMPTION; 4.1. Subsumption for nonlinear procedures; 4.2. Subsumption for linear procedures; 4.3. Summary; CHAPTER 5. RESOLUTION WITH EQUALITY; 5.1. Paramodulation; 5.2. Paramodulation and setting refinements; 5.3. Paramodulation and linear refinements; 5.4. Summary; CHAPTER 6. RESOLUTION AND PROBLEM REDUCTION FORMAT; 6.1. The problem reduction format

6.2. The ME procedure and problem reduction6.3. Summary; APPENDIX: Resolution-based procedures; REFERENCES; TABLE OF SYMBOLS; INDEX