Automating the Meta Theory of Deductive Systems

摘要

This thesis describes the design of a meta-logical framework that supports the representation and verification of deductive systems, its implementation as an automated theorem prover, and experimental results related to the areas of programming languages, type theory, and logics. Design: The meta-logical framework extends the logical framework LF HHP93 by a meta-logic M(2)(+). This design is novel and unique since it allows higher-order encodings of deductive systems and induction principles to coexist. On the one hand, higher-order representation techniques lead to concise and direct encodings of programming languages and logic calculi. Inductive definitions on the other hand allow the formalization of properties about deductive systems, such as the proof that an operational semantics preserves types or the proof that a logic is consistent. M(2)(+) is a proof calculus whose proof terms are recursive functions that may be defined by cases and range over dependent higher-order types. The soundness of M(2)(+) follows from a realizability interpretation of proof terms as total recursive functions. Implementation: A proof search algorithm for proof terms in M(2)(+) is implemented in the met a theorem prover that is part of the Twelf system PS99b. Its takes full advantage of higher-order encodings while using inductive reasoning.