Automated Theorem Proving: A Logical Basis

Preface

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.3.1. The Monkey-Banana Problem

1.3.2. Plane Geometry

1.3.3. Group Theory

1.3.4. Elementary Number Theory

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 Resolution

3.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 Reduction

6.3. Summary

Appendix: Resolution-Based Procedures

References

Table of Symbols

Index