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:
| Instead of | ∧ | ∨ | → | ↑ | ¬ | ∀ | ∃ | ⊥ |
|---|---|---|---|---|---|---|---|---|
| you can write | & | | | -> | ^ | ~ | ! | ? | False |
Just put each assumption and conclusion on its own line, i.e. press enter after each of them.
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.
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.
Mostly Joachim Breitner, with valuable help from some colleagues and friends.
For more information about the Incredible Proof Machine, especially from an academic point of view, please see the following publications:
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.