Order-Sorted Type Theory 1 : Unification

Abstract

The introduction of sorts to first-order ATP has brought a considerable gain in efficiency by reducing the search spaces, therefore it is desirable to be able to treat sorts in higher-order theorem proving in a similar way. In this paper we develop a sorted version of type theory; we extend the syntax and semantics of simple type theory by a higher-order sort concept that includes term declarations. In our system the partial ordering on the base sorts induces a partial ordering on the higher types by covariance in the rangesort and the natural inclusion of base function sorts. We present a set of transformations for sorted (pre-) unification and prove the nondeterministic completeness of the algorithm induced by these transformations.