Automating the meta theory of deductive systems
Carsten Elmar Schurmann, Frank Pfenning · 2000
Higher-order abstract syntax is a central representation technique in logical frameworks which maps variables of the object language into variables of the meta language. On the one hand, encodings using this idea are often extremely concise and elegant, on the other, higher-order representations are no longer inductive, which means that standard techniques for reasoning by induction do not apply. In this proposal, we present a meta-logic for LF (M! ) which overcomes this problem by representing inductive proofs as total functions. It uses recursion and pattern-matching to mimic strong induction principles. Because of the elegant representation of proofs it is possible to devise an efficient proof search algorithm for a fragment M 2 of M! . It has been implemented as an automated theorem prover for the proof assistant Twelf, a reimplementation and extension of the logic programming language Elf. Twelf has been used to prove fully automatically (among others) type preservation for Mini-M...