Construction and deduction in type theories
Auch gedruckt in der BibliothekI: J-H 5.236 ; W: W-H 6.168
FakultätFakultät für Informatik
Ressourcen- / MedientypDissertation, Text
Datum der Freischaltung1999-09-17
This dissertation is concerned with interactive proof construction and automated proof search in type theories, in particular the Calculus of Construction and its subsystems. Type theories can be conceived as expressive logics which combine a functional programming language, strong typing and a higher-order logic. They are therefore a suitable formalism for specification and verification systems. However, due to their expressiveness, it is difficult to provide appropriate deductive support for type theories. This dissertation first examines general methods for proof construction in type theories and then explores how these methods can be refined to yield proof search procedures for specialized fragments of the language. Proof development in type theories usually requires the construction of a term having a given type in a given context. For the term to be constructed, a metavariable is introduced which is successively instantiated in the course of the proof. A naive use of metavariables leads to problems, such as non-commutativity of reduction and instantiation and the generation of ill-typed terms during reduction. For solving these problems, a calculus with explicit substitutions is introduced, and it is shown that this calculus preserves properties such as strong normalization and decidability of typing. In order to obtain a calculus appropriate for proof search, the usual natural deduction presentation of type theories is replaced by a sequent style presentation. It is shown that the calculus thus obtained is correct with respect to the original calculus. Completeness (proved with a cut-elimination argument) is shown for all predicative fragments of the lambda cube. The dissertation concludes with a discussion of some techniques that make proof search practically applicable, such as unification and pruning of the proof search space by exploiting impermutabilities of the sequent calculus.
LizenzStandard (Fassung vom 03.05.2003)
LCSHLogic, symbolic and mathematical