Automated theorem proving in a simple meta-logic for LF
- 1 January 1998
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 286-300
- https://doi.org/10.1007/bfb0054266
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 meta-logic 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.Keywords
This publication has 7 references indexed in Scilit:
- Rules of definitional reflectionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Unification and anti-unification in the calculus of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A logic for reasoning with higher-order abstract syntaxPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Automated theorem proving in a simple meta-logic for LFLecture Notes in Computer Science, 1998
- Pi: An interactive derivation editor for the calculus of partial inductive definitionsLecture Notes in Computer Science, 1994
- A framework for defining logicsJournal of the ACM, 1993
- An algorithm for testing conversion in type theoryPublished by Cambridge University Press (CUP) ,1991