Applet for Cut-Elimination and Normalisation

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.

• CL - cut-elimination in classical logic
• LJT - cut-elimination in intuitionistic logic
• ND - normalisation in intuitionistic natural deduction

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.

• CL - cut-elimination in classical logic
• LJT - cut-elimination in intuitionistic logic
• ND - normalisation in intuitionistic natural deduction