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.