Hets: download and installation
Installers for Hets
needs Sun Java 1.4.2 or later (install with java -jar file.jar)
The installer is available forA Hets-Live-CD is available for download,too.
It runs on any computer with x86 architecture. Just boot from the CD. The most recent Hets-Live-CD is based on Slax.
Hets binaries are available here:
(these are not needed if you used one of the installers from above)- Linux daily snapshot latest release all versions
- x86_64 Linux daily snapshot latest release all versions
- (Leopard) PPC Mac daily snapshot latest release all versions
- (Leopard) Intel Mac daily snapshot latest release all versions
- PC Solaris daily snapshot latest release all versions
How to use a hets binary:
Just download the binary and put it somewhere in the $PATH.- Our current linux binaries also rely on gtk-2 and glade-2 libraries for more and better menus. Thus you may need to install additional libraries. (Use ldd on the hets binary to see which libraries are missing.)
- Daily Intel Mac (32bit) binaries for Leopard (OS X 10.5) (after 2009-11-19) also rely on the gtk2-framework (originally copied from r.research.att.com) that needs to be installed as root. (Use "otools -L hets" to see what the hets binary needs.) The binaries also work on 64bit or Snow-Leopard (OS X 10.6) Intel Macs.
- For displaying development graphs (with the -g option), you need to install uDraw(Graph) (formerly known as daVinci) that relies on Tcl/Tk (version 8.4) (which probably has been already installed on your computer anyway). Set $UNIWISH to the wish binary (which is part of Tcl/Tk), and $UNIDAVINCI to the uDrawGraph binary (if they are not in your $PATH). Tcl/Tk version 8.5 may also work.
- For Macs a wish binary is part of uDraw(Graph) in uDrawGraph-3.1/bin/Frameworks/Tk.framework/Versions/8.4/Resources/Wish.app/Contents/MacOS/Wish
Hets is called with
hets filename.casl
or
hets filename.het
For entering the command line mode, just call
hets
For a short description of the options, call
hets --help
How to install software needed for theorem proving with Hets:
- For interactive theorem proving you may install Isabelle and set $HETS_ISABELLE to the Isabelle binary.
- For automatic theorem proving you may install SPASS and/or Darwin.
- For reasoning about OWL specifications you may install Pellet and set $PELLET_PATH to the directory containing the script pellet.sh.
- The connection of Hets to other theorem provers is under development
Author: Dr. Christian Maeder
| Last updated: November 19, 2009 |  |