## 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. https://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.

**Unless otherwise indicated, the views expressed in this thesis are those of the author and do not necessarily represent the views of the University of Wollongong.**