Classical and constructive logic interactive theorem prover

This project is a classical and constructive logic interactive theorem prover. It is meant to help introduce users to sequent calculus and Gentzen trees. Given a logical statement, the user can click on a compound proposition (formula) to derive a statement that can either be another compound proposition or an atomic formula. The process continues until we reach an axiom, hence proving the truth of the original statement. This means that the program can for example prove that there exists a path between a and c, given a graph a-b-c. The challenge has been providing an imperative paradigm to what is usually done in functional programming.

 

Watch video | Printable poster [.pdf] 

  • Author

    Samar Rahmouni

  • Advisor

    Giselle Reis

Post a comment

Your email address will not be published. Required fields are marked *