Natural Deduction

This applet is also available on android.


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: 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