#### Year

1996

#### Degree Name

Master of Science (Hons.)

#### Department

Department of Mathematics

#### Recommended Citation

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

#### Abstract

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.