Secure CheckoutPersonal information is secured with SSL technology.
Free ShippingFree global shipping
No minimum order.
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.
2 Many-Sorted Resolution and Paramodulation
3 Formal Preliminaries for the RP-Calculus
4 Formal Preliminaries for the ∑RP-Calculus
5 Many-Sorted Term Rewriting
6 Completeness of the ∑RP-Calculus - The Ground Case
7 Many-Sorted Unification
8 Completeness of the ∑RP-Calculus - The General Case
9 Soundness of the ∑RP-Calculus
10 The Sort Theorem
11 An Automated Theorem Prover for the ∑RP-Calculus
12 Some Experiences with a Many-Sorted Theorem Prover
13 Related Work and Concluding Remarks
- No. of pages:
- © Morgan Kaufmann 1987
- 1st January 1987
- Morgan Kaufmann
- eBook ISBN:
Elsevier.com visitor survey
We are always looking for ways to improve customer experience on Elsevier.com.
We would like to ask you for a moment of your time to fill in a short questionnaire, at the end of your visit.
If you decide to participate, a new browser tab will open so you can complete the survey after you have completed your visit to this website.
Thanks in advance for your time.