Lightweight Lemmas in Lambda Prolog (Extended Version)
Lambda Prolog is known to be well-suited for expressing and implementing
logics and inference systems. We show that lemmas and definitions in
such logics can be implemented with a great economy of expression.
We encode a polymorphic higher-order logic using the ML-style
polymorphism of Lambda Prolog.
The terms of the metalanguage (Lambda Prolog) can be used to express the
statement of a lemma, and metalanguage type-checking can
directly type-check the lemma. But to allow polymorphic
lemmas requires either more general polymorphism at the meta-level or
a less concise encoding of the object logic. We discuss both the
Terzo and Teyjus implementations of Lambda Prolog as well as related
systems such as Elf.
A shorter version of this paper is to appear in
16th International Conference on Logic Programming, November 1999.