Automated Theorem Proving: A Logical Basis (eBook)
418 Seiten
Elsevier Science (Verlag)
978-1-4832-9677-7 (ISBN)
Automated Theorem Proving: A Logical Basis
Front Cover 1
Automated Theorem Proving: A Logical Basis 4
Copyright Page 5
Table of Contents 11
Dedication 6
PREFACE 7
ACKNOWLEDGEMENTS 13
CHAPTER 1. THE ROLE OF LOGICAL SYSTEMS 15
1.1. Orientation 15
1.2. The basic concepts of first-order logic 23
1.3. The formal presentation of problems 33
1.4. Refutation procedures 43
1.5. Preparation of formulas 46
1.6. The Herbrand Theorem 60
1.7. Summary 64
CHAPTER 2. BASIC RESOLUTION 66
2.1. Introduction 66
2.2. The Davis-Putnam Procedure 66
2.3. Ground resolution 70
2.4. Semantic Trees 80
2.5. General resolution: Unification 87
2.6. The general resolution procedure 97
2.7. Summary 107
CHAPTER 3. REFINEMENTS OF RESOLUTION 108
3.1. Introduction 108
3.2. Unit preference and set-of-support 112
3.3. Ordered clause deductions 120
3.4. Setting refinements 130
3.5. Linear refinements 155
3.6. Model elimination 183
3.7. Summary 213
CHAPTER 4. SUBSUMPTION 214
4.1. Subsumption for nonlinear procedures 214
4.2. Subsumption for linear procedures 251
4.3. Summary 275
CHAPTER 5. RESOLUTION WITH EQUALITY 277
5.1. Paramodulation 277
5.2. Paramodulation and setting refinements 293
5.3. Paramodulation and linear refinements 303
5.4. Summary 347
CHAPTER 6. RESOLUTION AND PROBLEM REDUCTION FORMAT 349
6.1. The problem reduction format 349
6.2. The ME procedure and problem reduction 373
6.3. Summary 404
APPENDIX: Resolution-based procedures 406
REFERENCES 409
TABLE OF SYMBOLS 414
INDEX 415
| Erscheint lt. Verlag | 19.8.2016 |
|---|---|
| Sprache | englisch |
| Themenwelt | Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge |
| Informatik ► Theorie / Studium ► Algorithmen | |
| Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik | |
| Mathematik / Informatik ► Mathematik | |
| Technik | |
| ISBN-10 | 1-4832-9677-6 / 1483296776 |
| ISBN-13 | 978-1-4832-9677-7 / 9781483296777 |
| Informationen gemäß Produktsicherheitsverordnung (GPSR) | |
| Haben Sie eine Frage zum Produkt? |
PDF (Adobe DRM)Kopierschutz: Adobe-DRM
Adobe-DRM ist ein Kopierschutz, der das eBook vor Mißbrauch schützen soll. Dabei wird das eBook bereits beim Download auf Ihre persönliche Adobe-ID autorisiert. Lesen können Sie das eBook dann nur auf den Geräten, welche ebenfalls auf Ihre Adobe-ID registriert sind.
Details zum Adobe-DRM
Dateiformat: PDF (Portable Document Format)
Mit einem festen Seitenlayout eignet sich die PDF besonders für Fachbücher mit Spalten, Tabellen und Abbildungen. Eine PDF kann auf fast allen Geräten angezeigt werden, ist aber für kleine Displays (Smartphone, eReader) nur eingeschränkt geeignet.
Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen eine
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen eine
Geräteliste und zusätzliche Hinweise
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.
aus dem Bereich
