Interactive Theorem Proving

My honours project was on the topic of interactive theorem proving. I was supervised by Professor John Crossley and Iman Poernomo. The aim of the project was to design a user interface for a theorem proving program that is simple to use, while being applicable to a large range of logics. The result is a prototypical program named Igloo.

Using the links on the top left corner of these pages, you can read about the internal design of Igloo, or see some screenshots of a sample proof. There are also downloadable versions of my thesis and other documents.