The HLM Proof Assistant

Prototype

Click here to download the HLM prototype and library.

(Last update: February 8, 2011)

Note: This prototype is intended as a proof of concept; it cannot be used as an actual proof assistant yet. Also, most of the library has been written manually in XML, and cannot be reproduced in the GUI yet.

Requirements:

• Windows, MacOS, or Linux. (Note: Only the Linux version is tested regularly.)
• A reasonably up-to-date Java runtime (the official Oracle JRE, OpenJDK, or GCJ).
• The version of the SWT toolkit appropriate for your platform. (3.6.1 is known to work; look for a 64-bit build if you have a 64-bit Java runtime.)
• Optionally: GNU FreeFont, to make mathematical symbols prettier.

Extract hlm.jar and swt.jar into the same directory, then run hlm.jar as follows:

• Windows: Execute the file by double-clicking.
• Linux: Run java -jar hlm.jar from a terminal.
• MacOS: Run java -XstartOnFirstThread -jar hlm.jar from a terminal.

Then extract library.hlm to a writable directory and open it in HLM.

SVN Access

Check out both the source code and the library from:

https://hlm.svn.sourceforge.net/svnroot/hlm/trunk

The easiest way to compile HLM is from the Eclipse IDE. First set up a classpath variable SWT pointing at the appropriate .jar file somewhere in the Eclipse directory (because Eclipse uses SWT). Then choose "File / Import / Existing projects into workspace," select the java subdirectory of HLM as the root directory, and import all projects it contains. This should also import some run configurations that can be accessed via "Run / Run configurations."

In the GUI, load the file Library.xml from the library subdirectory.