Automated Theorem Proving: A Logical Basis - 1st Edition - ISBN: 9780720404999, 9781483296777

Automated Theorem Proving: A Logical Basis

1st Edition

Authors: D.W. Loveland
eBook ISBN: 9781483296777
Imprint: North Holland
Published Date: 1st January 1978
Page Count: 418
Tax/VAT will be calculated at check-out Price includes VAT (GST)
54.95
72.95
43.99
Unavailable
Price includes VAT (GST)
× DRM-Free

Easy - Download and start reading immediately. There’s no activation process to access eBooks; all eBooks are fully searchable, and enabled for copying, pasting, and printing.

Flexible - Read on multiple operating systems and devices. Easily read eBooks on smart phones, computers, or any eBook readers, including Kindle.

Open - Buy once, receive and download all available eBook formats, including PDF, EPUB, and Mobi (for Kindle).

Institutional Access

Secure Checkout

Personal information is secured with SSL technology.

Free Shipping

Free global shipping
No minimum order.

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

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.


Details

No. of pages:
418
Language:
English
Copyright:
© North Holland 1978
Published:
Imprint:
North Holland
eBook ISBN:
9781483296777

About the Authors

D.W. Loveland Author