---
title: "A Many-Sorted Calculus Based on Resolution and Paramodulation"
authors:
  - "Christoph Walther"
doi: ""
url: "https://ijcai.org/proceedings/1983/211"
pdf: "https://ijcai.org/proceedings/1983/0211.pdf"
venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence"
year: 1983
pages: "882-890"
track: "Theorem Proving"
keywords:
---

# A Many-Sorted Calculus Based on Resolution and Paramodulation

Christoph Walther

*Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 882-890.

## Abstract

The first-order ca l c ulus whose well formed formulas are clauses and whose sole inference rules are factorization, resolution and paramodulation is extended to a many-sorted calculus. As abasis for Automated Theorem Proving, this many-sorted calcu lus le ads to a remarka ble reduction of thesearch space and also to simpler proofs. The soundness and completeness of th e new ca lculus and the Sort-Theorem, which relate s t he many-sorted c alculus to its one -s o rt ed cou nterpart, are shown. Inaddition results about term rewriting a nd unification in a many-sorted calculus are obtained. Pra ctical examp l es and a proof protocol of an automated th eorem proverbased on the many-sorted calculus a re presented.