Walther A Many-Sorted Calculus Based on Resolution and Paramodulation

1. Auflage 2014
ISBN: 978-1-4832-5893-5
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 170 Seiten, Web PDF

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.

Autoren/Hrsg.

Walther, Christoph

Inhaltsverzeichnis

1;Front Cover;1
2;A Many-Sorted Calculus Based on Resolution and Paramodulation;4
3;Copyright Page;5
4;Table of Contents;6
5;Notation;7
6;Preface;8
7;Chapter 1. Introduction;10
7.1;Many-Sorted Calculi;11
7.2;The Many-Sorted Language;12
7.3;Semantics;13
7.4;Inference Rules;14
7.5;Efficiency of many-sorted reasoning;15
8;Chapter 2. Many-Sorted Resolution and Paramodulation;20
8.1;Many-Sorted Resolution and Factorization;22
8.2;Many-Sorted Paramodulation;31
8.3;Many-sorted Axiomatizations;38
9;Chapter 3. Formal Preliminaries for the RP-Calculus;43
9.1;Syntactic Notions;43
9.2;Substitutions and Unifiers;44
9.3;Subterm Selectors;46
9.4;Term Rewriting;47
9.5;Inference Rules and Deductions;48
9.6;Semantic Notions;49
10;Chapter 4. Formal Preliminaries for the SRP-Calculus;50
10.1;Sorts and Signatures;50
10.2;Syntactic Notions;51
10.3;Substitutions and Unifiers;53
10.4;Term Rewriting;55
10.5;Inference Rules and Deductions;55
10.6;Semantic Notions;56
11;Chapter 5. Many-Sorted Term Rewriting;57
12;Chapter 6. Completeness of the SRP-Calculus – The Ground Case;70
13;Chapter 7. Many-Sorted Unification;80
14;Chapter 8. Completeness of the SRP-Calculus – The General Case;98
15;Chapter 9. Soundness of the SRP-Calculus;110
16;Chapter 10. The Sort Theorem;114
17;Chapter 11. An Automated Theorem Prover for the SRP-Calculus;126
17.1;The Input Language;126
17.2;The Compiler;128
17.3;The Skolemization Routine;129
17.4;The Unification Algorithm;132
17.5;Computation of Resolvents. Factors and Paramodulants;138
18;Chapter 12. Some Experiences with a Many-Sorted Theorem Prover;142
19;Chapter 13. Related Work and Concluding Remarks;159
20;References;163