Automated Theorem Proving in a Simple Meta-Logic for LF

Abstract. 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 metalogic M2 which allows inductive reasoning over 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.

• Type: Conference
• Year: 1998
• Where: CADE
• Authors: Carsten Schürmann, Frank Pfenning
• Keywords: CADE 1998, LF Encodings, Logical Framework Lf, Logical Reasoning, Programming Languages