Many-Sorted Calculus Based on Resolution and Paramodulation (eBook)
170 Seiten
Elsevier Science (Verlag)
9781483258935 (ISBN)
A Many-Sorted Calculus Based on Resolution and Paramodulation emphasizes the utilization of advantages and concepts of many-sorted logic for resolution and paramodulation based automated theorem proving. This book considers some first-order calculus that defines how theorems from given hypotheses by pure syntactic reasoning are obtained, shifting all the semantic and implicit argumentation to the syntactic and explicit level of formal first-order reasoning. This text discusses the efficiency of many-sorted reasoning, formal preliminaries for the RP- and ?RP-calculus, and many-sorted term rewriting and unification. The completeness and soundness of the ?RP-calculus, sort theorem, and automated theorem prover for the ?RP-calculus are also elaborated. This publication is a good source for students and researchers interested in many-sorted calculus.
Front Cover 1
A Many-Sorted Calculus Based on Resolution and Paramodulation 4
Copyright Page 5
Table of Contents 6
Notation 7
Preface 8
Chapter 1. Introduction 10
Many-Sorted Calculi 11
The Many-Sorted Language 12
Semantics 13
Inference Rules 14
Efficiency of many-sorted reasoning 15
Chapter 2. Many-Sorted Resolution and Paramodulation 20
Many-Sorted Resolution and Factorization 22
Many-Sorted Paramodulation 31
Many-sorted Axiomatizations 38
Chapter 3. Formal Preliminaries for the RP-Calculus 43
Syntactic Notions 43
Substitutions and Unifiers 44
Subterm Selectors 46
Term Rewriting 47
Inference Rules and Deductions 48
Semantic Notions 49
Chapter 4. Formal Preliminaries for the SRP-Calculus 50
Sorts and Signatures 50
Syntactic Notions 51
Substitutions and Unifiers 53
Term Rewriting 55
Inference Rules and Deductions 55
Semantic Notions 56
Chapter 5. Many-Sorted Term Rewriting 57
Chapter 6. Completeness of the SRP-Calculus – The Ground Case 70
Chapter 7. Many-Sorted Unification 80
Chapter 8. Completeness of the SRP-Calculus – The General Case 98
Chapter 9. Soundness of the SRP-Calculus 110
Chapter 10. The Sort Theorem 114
Chapter 11. An Automated Theorem Prover for the SRP-Calculus 126
The Input Language 126
The Compiler 128
The Skolemization Routine 129
The Unification Algorithm 132
Computation of Resolvents. Factors and Paramodulants 138
Chapter 12. Some Experiences with a Many-Sorted Theorem Prover 142
Chapter 13. Related Work and Concluding Remarks 159
References 163
| Erscheint lt. Verlag | 10.7.2014 |
|---|---|
| Sprache | englisch |
| Themenwelt | Mathematik / Informatik ► Mathematik |
| Technik | |
| ISBN-13 | 9781483258935 / 9781483258935 |
| 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
