A Many-Sorted Calculus with Polymorphic Functions Based On Resolution And Paramodulation

Abstract

A many-sorted first order calculus, called ΣRP, whose well formed formulas are sorted (typed) clauses and whose inference rules are factorization, resolution, paramodulation and weakening is extended to a many sorted calculus ΣRP* with polymorphic functions (overloading). It is assumed that the sort structure is a finite partially ordered set with a greatest element. It is shown, that this extended calculus is sound and complete, provided the functional reflexivity axioms are present. It is also shown, that unification of terms containing polymorphic functions is in general finitary, i.e. the set of most general unifiers may contain more than one element, but at most finitely many. We give a natural condition for the signature (the sort structure), such that the set of most general unifiers is always at most a singleton provided this condition holds.