Project Abstract

Firstly, to improve reasoning and making good valid argument, secondly, for efficient program extraction, the Howard curry correspondence allows correct by construction program from proof, creating safer and guaranteed to be correct software. Lastly Logic is as important as maths and English.The main aim of this project is to add advanced tactics to make theorem proving efficient, and hopefully more fun. The main approach to this project is simply studying logics and proofs, and studying Haskell programming language; I looked into different proof system that exists. For this project, my primary goal was to make the software more efficient for theorem proving; to do this i have incorporated tactics that allow easier form of theorem proving.This is a niche topic that which I am focusing. In terms of the contribution, I would say that it will prove theorem proving, and due to program extraction and Howard curry correspondence; we can derive a program that is guaranteed to be correct

Keywords: Proof Logic Prawf, Proof Assistant Natural Deduction, Therom proving P or Not P?

 Conference Details

Session: Poster Session B at Poster Stand 31

Location: Sir Stanley Clarke Auditorium at Wednesday 8th 09:00 – 12:30

Markers: Ulrich Berger, Mark Jones

Course: BSc Computer Science, 3rd Year

Future Plans: I’m looking for work