Published on *Computer Science Department at Princeton University* (http://www.cs.princeton.edu)

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.

**Links**

[1] http://www.cs.princeton.edu/research/techreps/author/371

[2] http://www.cs.princeton.edu/research/techreps/author/45

[3] ftp://ftp.cs.princeton.edu/techreports/1999/607.ps.gz