Lambda Calculator (version 0.2)

Abstract

The Lambda Calculator is a proof finding program based on Martin Bunder's article Proof finding algorithms for implicational logics. It finds proofs (lambda terms) for propositions of implicational intuitionistic logic (SK logic) and several sub-intuitionistic logics (e.g. BCK,BCI,BCIW). Other connectives can be defined using a falsum type. When axioms like ex-falso and Peirce's law are added, the program also finds proofs for propositions of classical logic.

Other features of this program include: finding the principal type of lambda terms, and translating lambda terms to combinatory terms (using only combinators that are definable in the given logical system). The translation algorithms can be found in Bunder's article Lambda terms definable as combinators.

Much of the code was inspired by Tony Dekker's program Brouwer. The Lambda Calculator was implemented using the functional language Clean.

Download