Bogdan Ciobanu Undergraduate Dissertation 2015/16

A Simple Proof Checker for Propositional Logic

Supervised by G.Struth

Abstract

Logic has been the tool used by professionals to reason about various situations and also construct arguments around. In order to build accurate arguments, a language was developed to express sentences from a logical perspective. 

The language this research paper is going to revolve around, is propositional logic. It consists of propositions that one can argue as of being true or false. 

Several propositions are going to embody a proof, which analogously has a truth value. The scope of this project is to design and implement a Haskell-based proof checker, following a series of defined steps, that is going to test proofs inputed by the user. 

Haskell, quite well-known as being a pure functional programming language, is going to model each step. The reason it was chosen against all the others is its consistent programming style. Using a recursive approach, Haskell is going to be very practical in implementing more-bug free code in less time.