Quick links

Lightweight Lemmas in Lambda Prolog (Extended Version)

Report ID:
September 1999
Download Formats:


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.

Follow us: Facebook Twitter Linkedin