A theorem prover “reasonEq” , written in Haskell, is currently under development. It is intended to support reasoning about the meaning and correctness of programs. It supports an easy to use proof style for predicate calculus known as “equational reasoning” – very similar to the kind of algebraic reasoning used in most mathematics found in undergraduate courses. It currently has a command-line/REPL style user interface, and a prototype GUI.
It’s hosted on Github: https://github.com/andrewbutterfield/reasonEq
Project ideas include:
- Using the prover to build a useful library of theories, as well as giving feedback on features and user interface.
- Extending the prover by adding in proof automation function to try various strategies to find proofs.
- Improving the display of theorems and proofs
- Exploring the connection of the theorem-prover to The TPTP Problem Library for Automated Theorem Proving ( https://www.tptp.org/ ) – Masters level.
Projects can be scoped for both 4th year projects and year 5 dissertations