Lightweight Lemmas in Lambda Prolog (Extended Version)
Report ID: TR-607-99Author: Felty, Amy P. / Appel, Andrew W.
Date: 1999-10-00
Pages: 26
Download Formats: |Postscript|
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.