Lightweight Lemmas in Lambda Prolog (Extended Version)
Abstract:
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.