A Many-Sorted Calculus Based on Resolution and Paramodulation
- 1st Edition - July 10, 2014
- Imprint: Morgan Kaufmann
- Author: Christoph Walther
- Language: English
- Paperback ISBN:9 7 8 - 0 - 2 7 3 - 0 8 7 1 8 - 2
- eBook ISBN:9 7 8 - 1 - 4 8 3 2 - 5 8 9 3 - 5
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… Read more
Purchase options
Institutional subscription on ScienceDirect
Request a sales quoteA 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.
Notation1 Introduction2 Many-Sorted Resolution and Paramodulation3 Formal Preliminaries for the RP-Calculus4 Formal Preliminaries for the ∑RP-Calculus5 Many-Sorted Term Rewriting6 Completeness of the ∑RP-Calculus - The Ground Case7 Many-Sorted Unification8 Completeness of the ∑RP-Calculus - The General Case9 Soundness of the ∑RP-Calculus10 The Sort Theorem11 An Automated Theorem Prover for the ∑RP-Calculus12 Some Experiences with a Many-Sorted Theorem Prover13 Related Work and Concluding RemarksReferences
- Edition: 1
- Published: July 10, 2014
- Imprint: Morgan Kaufmann
- Language: English
- Paperback ISBN: 9780273087182
- eBook ISBN: 9781483258935
Read A Many-Sorted Calculus Based on Resolution and Paramodulation on ScienceDirect