Applet for Cut-Elimination and NormalisationWarning: These pages are still under construction and designed for the conoscenti only. If you encounter any problems, email me. Some general information about the applet is given below.
The applet is outcome of my interest in cut-elimination. It helps to explore reduction trees in a slight variant of the sequent calculus LK, and also reduction trees in Herbelin's calculus LJT (as presented here) and in the standard formulation of natural deduction for intuitionistic logic. Given for example the following classical sequent proof
you can produce by simply pressing the buttons L and R the following two cut-free proofs.
If you ever have done cut-elimination by hand, then you know how useful this applet is.
The applet is particularly useful for doing some calculations finding out what the (proof-theoretical) semantics for classical logic should look like. Some informal notes are here.
The applet needs at least Java 1.2 including the Swing libraries. Some browsers support these requirements directly, and if you are one of the lucky to have such a browser you can access the three calculi by pressing on one of the following links.
If not, then your browser can most probably run the applet with the help of a Java plugin. In this case follow the links below.
|For the curious: the applet is written in MLJ, which is being developed by Benton, Kennedy and Russo. MLJ is a dialect of SML that provides access to Java libraries; in my opinion it is a really nifty language! I am using an improved version of the MLJ-0.2 compiler.|
Last modified: Sat Mar 3 05:16:36 CET 2007