Polymorphic lemmas and definitions in Lambda Prolog and Twelf

TL;DR

This paper demonstrates efficient encoding of lemmas and definitions in higher-order logic using Lambda Prolog and Twelf, comparing their features and implementation benefits for expressing logics and inference systems.

Contribution

It introduces a novel encoding approach for higher-order logic in Lambda Prolog and compares it with Twelf, highlighting the expressive economy and implementation differences.

Findings

Lambda Prolog effectively encodes higher-order logic with concise syntax

Comparison shows strengths and limitations of Lambda Prolog and Twelf for logic encoding

Encoding approach simplifies lemma and definition implementation in logic systems

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 higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage (Lambda Prolog). We discuss both the Terzo and Teyjus implementations of Lambda Prolog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.