### Natural Deduction

This applet is also available on android.

### Goal

The goal is to build a proof tree in natural deduction of the proposition displayed at the bottom of the big black panel. The proof is built by clicking on formulae. The program decides which rule to apply as follows:
• If the clicked formula is a leaf of a proof tree and
• its top operator is a ∧, the rule for conjunction introduction is applied.
• its top operator is a ∨, the first rule for disjunction introduction is applied. A second click on the same formula applies the second rule.
• its top operator is a ->, the rule for implication introduction is applied.
• its top operator is a ¬, the rule for negation introduction is applied.
• it is atomic, an attachement to a root of another tree is performed. The roots to which it can be attached are coloured in red. If there are more that one root, the attachment needs to be explicited by dragging the mouse to the desired root.
• If the clicked formula is the root of a proof tree and
• its top operator is a ∧, the first rule for conjunction elimination is applied. A second click on the same formula applies the second rule.
• its top operator is a ∨, the rule for disjunction elimination is applied with an attachment to a leaf of another tree. The leaves to which it can be attached are coloured in red. If there are more that one leaf , the attachment needs to be explicited by dragging the mouse to the desired leaf.
• its top operator is a ->, the rule for implication elimination is applied.
• its top operator is a ¬, the rule for negation elimination is applied.
• its top operator is a , the rule for false elimination is applied with an attachment to a leaf of another tree. The leaves to which it can be attached are coloured in red. If there is more that one leaf, the attachment is explicited by dragging the mouse to the desired leaf.
• it is atomic, an attachement to a leaf of another tree is performed. The leaves to which it can be attached are coloured in red. If there are more that one leaf, the attachment needs to be explicited by dragging the mouse to the desired leaf.
When an introduction rule adds an assumption to the context. This assumption in the proof tree is coloured in blue. Clicking on a blue formula creates a new proof tree whose root is the assumption.
The application of rule can be canceled by clicking on the same formula that trigers the application.
This applet has been tested with Java 1.4.2 (Sun). Check your version of java
Laurent Théry