Higher-Order Order-Sorted Resolution

Abstract

The introduction of sorts to first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search space. It is therefore promising to treat sorts in higher order theorem proving as well. In this paper we present a generalization of Huet’s Constrained Resolution to an order-sorted type theory ΣT with term declarations. This system builds certain taxonomic axioms into the unification and conducts reasoning with them in a controlled way. We make this notion precise by giving a relativization operator that totally and faithfully encodes ΣT into simple type theory.