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!
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.
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 obvoiusly 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:
you can write
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.
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.