Konferenzartikel: Visual theorem proving with the Incredible Proof Machine

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.