A Many-Sorted Calculus Based on Resolution and Paramodulation - 1st Edition - ISBN: 9780273087182, 9781483258935

A Many-Sorted Calculus Based on Resolution and Paramodulation

1st Edition

Authors: Christoph Walther
eBook ISBN: 9781483258935
Imprint: Morgan Kaufmann
Published Date: 1st January 1987
Page Count: 170
Sales tax will be calculated at check-out Price includes VAT/GST
15% off
15% off
15% off
Price includes VAT/GST
× DRM-Free

Easy - Download and start reading immediately. There’s no activation process to access eBooks; all eBooks are fully searchable, and enabled for copying, pasting, and printing.

Flexible - Read on multiple operating systems and devices. Easily read eBooks on smart phones, computers, or any eBook readers, including Kindle.

Open - Buy once, receive and download all available eBook formats, including PDF, EPUB, and Mobi (for Kindle).

Institutional Access

Secure Checkout

Personal information is secured with SSL technology.

Free Shipping

Free 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.

Table of Contents


1 Introduction

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
Morgan Kaufmann
eBook ISBN:

About the Author

Christoph Walther

Ratings and Reviews