Theorem proving algorithms using lambda calculus and combinatory logic

The work of Martin Bunder [4] presents a simple version of the Ben - Yelles Algorithm as a tree. Given a formula of implicational logic, the algorithm determines the (possibly empty) set of X - terms w^hich have the given formula as a type. By the formulas as types isomorphism, it follows that this determines the set of its proofs. This is done in a finite numbers of steps. The algorithm which apphes to intuitionistic logic, has been extended to some weaker logics such as BCI, BCK etc. In this thesis we extend the Ben - Yelles algorithm to logics with connectives other than by using the axiom I- f ^ A, Peirce's law or both, i.e. to the logics with implication and intuitionistic negation, classical implicational logic and classical logic, as well as certain intermediate logics.