Master of Science (Hons.)
Department of Mathematics
Rizkalla, Ramzy Master, Theorem proving algorithms using lambda calculus and combinatory logic, Master of Science (Hons.) thesis, Department of Mathematics, University of Wollongong, 1996. http://ro.uow.edu.au/theses/2848
The work of Martin Bunder  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.