This applet implements an interactive tactical theorem prover for first-order logic. It combines Larry Paulson's original ML code with an ML parser for interpreting commands and a scrolling terminal window written in Java. The terminal code was adapted from the WebTerm applet written by Dianne Hackborn and Melanie Johnson at the Northwest Alliance for Computational Science and Engineering.
Click here for a brief guide to using Hal. It does assume familiarity with sequent calculus for first order logic.
Click here for an account of the way in which the code for this example is structured.
| MLj home | Comments to: mlj@dcs.ed.ac.uk |