Hal: A Tactical Theorem Prover

The core of this example was written by Larry Paulson and is described in Chapter 10 of his (highly recommended) book ML for the Working Programmer.

Applet should appear here but you don't have Java enabled in your browser.

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