The calculus of constructions as a framework for proof search with set variable instantiation (Q1575927)

It is shown how a procedure developed by Bledsoe for automatically finding substitution instances for set variables in higher-order logic can be adapted to provide increased automation in proof search in the Calculus of Constructions (CC). Bledoe's procedure operates on an extension of first-order logic that allows existential quantification over set variables. This class of variables can also be identified in CC. The existence of a correspondence between higher-order logic and higher-order type theories such as CC is well known. CC can be viewed as an extension of higher-order logic where the basic terms of the language, the simply-typed \(\lambda\)-terms are replaced with terms containing dependent types. It is shown how Bledsoe's techniques can be incorporated into a reformulation of a search procedure for CC given by Dowek and extended to handle terms with dependent types. A notion of search context for CC which allows smooth integration of the step which finds solutions to set variables. The procedure can be restricted to obtain procedures for set variable instantiation in sublanguages of CC such as the Logical Framework (LF) and higher-order hereditary Harrop formulas. The latter serves as the logical foundation of the \(\lambda\)Prolog logic programming language.