The Meta Theory of the Incredible Proof Machine

Joachim Breitner 🌐 and Denis Lohner 🌐

May 20, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The Incredible Proof Machine is an interactive visual theorem prover which represents proofs as port graphs. We model this proof representation in Isabelle, and prove that it is just as powerful as natural deduction.


BSD License


Session Incredible_Proof_Machine