The Incredible Proof Machine
Current task:
Block count:
Logic blocks:
Helper blocks:
New custom block:
Custom blocks:
What do you want to prove today?
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)!
[introductory
video on the Tea Leaves Programming channel (13min)](https://www.youtube.com/watch?v=bExGUtVWzb4)
Why is this?
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.
Which keyboard shortcuts can I use?
CTRL+Z: Undo change
CTRL+Y: Redo change
CTRL+A: Select all blocks
BACKSPACE, DELETE: Delete selected blocks
SHIFT+MOUSE1: Add block or region to selection
Why is the conclusion not green?
Because your proof is not a proof (yet). This can have these reasons:
Some of your blocks have an input (an assumption) that is not connected to
anything. These are red.
Some of your connections connect propositions that are obviously different (marked red and marked with
☠), or they are underspecified and it is not clear whether they might be different or not (marked red
and with ?). In the latter case, inserting an annotation block (✎P) can help.
You have cycles in the proof. These are (you guessed it) marked red.
You have wired up local hypotheses wrongly. Local hypotheses are those outputs that come out on the left
of a dent in the block, and can only be used in the part of the proof that connects to the corresponding
input on the right of the dent. Do I need to mention that these are marked red?
How do I enter these funny characters?
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:
How do I create a custom task with multiple assumptions or conclusions?
Just put each assumption and conclusion on its own line, i.e. press enter after each of them.
How do I create custom blocks?
You can select blocks in a proof by clicking them while holding down Shift. Then, the option to create a
custom block wrapping the ones you've selected will appear.
Where did my proofs go?
Currently, your proofs will only be saved in your own browser. This means they will be lost when you delete
your local storage after you close this window/tab, or if this is a private browsing session or similar. We
have plans to save your progress on our server in a future version.
Who did this?
Mostly Joachim Breitner, with valuable help from some colleagues and friends.
Where can I read more about this?
For more information about the Incredible Proof Machine, especially from an academic point of view, please
see the following publications:
Joachim Breitner: Visual
theorem proving with the Incredible Proof Machine, accepted paper at ITP 2016, August 2016
[Visual
theorem proving with the Incredible Proof Machine](https://www.joachim-breitner.de/publications/Incredible_ITP2016_preprint.pdf)
Joachim Breitner: The
Incredible Proof Machine, Invited talk at LFMTP 2016, June 2016
[The
Incredible Proof Machine](https://www.joachim-breitner.de/publications/Incredible_LFMTP_2016-06-23.pdf)
Joachim Breitner, Denis Lohner: The meta theory of the
Incredible Proof Machine, Isabelle formalisation in the Archive of Formal Proofs,
May 2016
[The meta theory of the
Incredible Proof Machine](http://isa-afp.org/entries/Incredible_Proof_Machine.shtml)
Incredible Proof Machine,
Interview of Joachim Breitner by Sebastian Ritterbusch, episode 78 of the science podcast
“Modellansatz”, German, 2016
Can I help?
Most certainly! Everything is Free Software, so you can jump right in, fetch the code and start contributing. The more people
contribute, the more incredible the The Incredible Proof Machine becomes.