Skip to main content

Use this tag for the tool The Incredible Proof Machine. The Incredible Proof Machine is a web-based tool for visually performing formal proofs.

The Incredible Proof Machine pdf is a tool to perform proofs in various logics visually. It employs a proof representation based on port graphs that is similar to natural deduction. Proof are performed by adding blocks and connecting them.

From info popup

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.

The first task is

enter image description here

The simplest correct solution is

enter image description here

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.

enter image description here

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.

enter image description here

You have cycles in the proof. These are (you guessed it) marked red.

enter image description here

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? Blocks can be extended in width.

enter image description here

enter image description here

Solutions