A mechanization of sorted higher-order logic based on the resolution principle

Abstract

The usage of sorts in first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search spaces involved. This suggests that sort information can be employed in higher-order theorem proving with similar results. This thesis develops a sorted higher-order logic SUM HOL suitable for automatic theorem proving applications. SUM HOL is based on a sorted Lambda-calculus SUM A->, which is obtained by extending Church';s simply typed Lambda-calculus by a higher-order sort concept including term declarations and functional base sorts. The term declaration mechanism studied here is powerful enough to allow convenient formalization of a large body of mathematics, since it offers natural primitives for domains and codomains of functions, and allows to treat function restriction. Furthermore, it subsumes most other mechanisms for the declaration of sort information known from the literature, and can thus serve as a general framework for the study of sorted higher-order logics. For instance, the term declaration mechanism of SUM HOL subsumes the subsorting mechanism as a derived notion, and hence justifies our special form of subsort inference. We present sets of transformations for sorted higher-order unification and pre-unification, and prove the nondeterministic completeness of the algorithm induced by these transformations. The main technical difficulty of unification in ! is that the analysis of general bindings is much more involved than in the unsorted case, since in the presence of term declarations well-sortedness is not a structural property. This difficulty is overcome by a structure theorem that links the structure of a formula to the structure of its sorting derivation. We develop two notions of set-theoretic semantics for SUM HOL. General SUM-models are a direct generalization of Henkin';s general models to the sorted setting. Since no known machine-oriented calculus can adequately mechanize full extensionality, we generalize general SUM-models further to SUM-model structures, which allow full extensionality to fail. The notions of SUM-model structures and general SUM-models allow us to prove model existence theorems for them. These model-theoretic variants of Andrews unifying principle for type theory'; can be used as a powerful tool in completeness proofs of higher-order calculi. Finally, we use our pre-unification algorithms as a central inference procedure for a sorted higherorder resolution calculus in the spirit of Huet';s Constrained Resolution. This calculus is proven sound and complete with respect to our semantics. It differs from Huet';s calculus by allowing early unification strategies and using variable dependencies. For the completeness proof we make use of our model existence theorem, and prove a strong lifting lemma.