Automated Theorem Proving: A Logical Basis
- 1st Edition - January 1, 1978
- Latest edition
- Author: D.W. Loveland
- Language: English
Fundamental Studies in Computer Science, Volume 6: Automated Theorem Proving: A Logical Basis aims to organize, augment, and record the major conceptual advances in automated… Read more
World Book Day celebration
Where learning shapes lives
Up to 25% off trusted resources that support research, study, and discovery.
Description
Description
Fundamental Studies in Computer Science, Volume 6: Automated Theorem Proving: A Logical Basis aims to organize, augment, and record the major conceptual advances in automated theorem proving. The publication first examines the role of logical systems and basic resolution. Discussions focus on the Davis-Putnam procedure, ground resolution, semantic trees, general resolution procedure, basic concepts of first-order logic, refutation procedures, and preparation of formulas. The text then takes a look at the refinements of resolution, including unit preference and set-of-support, ordered clause deductions, and setting and linear refinements. The monograph tackles subsumption, resolution with equality, and resolution and problem reduction format. Topics include problem reduction format, paramodulation and linear refinements, paramodulation, and subsumption for linear and nonlinear procedures. The publication is a dependable reference for students and researchers interested in automated theorem proving.
Table of contents
Table of contents
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
Product details
Product details
- Edition: 1
- Latest edition
- Published: January 1, 1978
- Language: English
View book on ScienceDirect
View book on ScienceDirect
Read Automated Theorem Proving: A Logical Basis on ScienceDirect