George O'Brien Undergraduate Dissertation 2015/16

Predicate Logic Proof Checker

Supervised by G.Struth

Abstract

The initial project is to design and build a predicate logic proof checker as well as explore other methods of automated proof. The designs of any of the implemented systems has been greatly simplified, in order to give a clear demonstration of how they work. Furthermore, these systems will be evaluated to give a rough idea of the differences in efficiency. Many of these algorithms are based on research of current automated proof tools, so these tools were analyzed before the design.