[breitner16incredible] | Joachim Breitner, Visual theorem proving with the Incredible Proof Machine, Interactive Theorem Proving, 2016.
|
Abstract
The Incredible Proof Machine is an easy and fun to use program to conduct formal proofs. It employs a novel, intuitive proof representation based on port graphs, which is akin to, but even more natural than, natural deduction. In particular, we describe a way to determine the scope of local assumptions and variables implicitly. Our practical classroom experience backs these claims.
Download
BibTeX
Authors at the institute