flâneur

The Incredible Proof Machine

incredible.pm · 635 words · saved by 1 readers

This is a tool to perform proofs in various logics (e.g. propositional, predicate logic) visually: You simply add blocks that represent the various proofs steps, connect them properly, and if the conclusion turns green, then you have created a complete proof! Simply drag and drop to connect two dots; for some examples of completed proofs, see this paper. For a quick introduction to the UI, check out the introductory video on the Tea Leaves Programming channel (13min)! The Incredible Proof Machine was created to convey the fun and joy of doing proofs, especially in a computer aided way, without first having to learn the syntax of a “real” thereom prover like Isabelle. Because your proof is not a proof (yet). This can have these reasons: There are only a few places where you actually have to enter formulas, mostly if you want to use the ✎P-block or define your own tasks. There, you can use the following abbreviations: Just put each assumption and conclusion on its own line, i.e. press en

Welcome to The Incredible Proof Machine! What is this? This is a tool to perform proofs in various logics (e.g. propositional, predicate logic) visually: You simply add blocks that represent the various proofs steps, connect them properly, and if the conclusion turns green, then you have created a complete proof! Simply drag and drop to connect two dots; for some examples of completed proofs, see this paper. For a quick introduction to the UI, check out the introductory video on the Tea Leaves Programming channel (13min)! Why is this? The Incredible Proof Machine was created to convey…

saved by

related reading