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