A many-sorted calculus based on resolution and paramodulation

Abstract

The first-order calculus whose well formed formulas are clauses and whose sole inference rules are factorization, resolution and paramodulation is extended to a many-sorted calculus. As a basis for Automated Theorem Proving, this many-sorted calculus leads to a remarkable reduction of the search space and also to simpler proofs. Soundness and completeness of the new calculus and the Sort-Theorem, which relates the many-sorted calculus to its one-sorted counterpart, are shown. In addition results about term rewriting and unification in a many-sorted calculus are obtained. The practical consequences for an implementation of an automated theorem prover based on the many-sorted calculus are described.