Automated Theorem Proving in a Simple Meta Logic for LF

. Higher-order representation techniques allow elegant encodings of logics and programming languages in the logical framework LF, but unfortunately they are fundamentally incompatible with induction principles needed to reason about them. In this paper we develop a meta-logic M2 which allows inductive reasoning over such LF encodings, and describe its implementation in Twelf, a special-purpose automated theorem prover for properties of logics and programming languages. We have used Twelf to automatically prove a number of non-trivial theorems, including type preservation for Mini-ML and the deduction theorem for intuitionistic propositional logic. 1 Introduction The logical framework LF [HHP93] has been designed as a meta-language for representing deductive systems which are common in the study of logics and programming languages. It allows concise encodings of many common inference systems, such as natural deduction and sequent calculi, type systems, operational semantics, compilers...