Hets: download and installation

Installers for Hets

needs Sun Java 1.4.2 or later (install with java -jar file.jar)

• x86 Linux
• PowerPC Mac (Tiger)
• x86 Mac (Leopard)
• Sparc Solaris
• x86 Solaris

A Hets-Live-CD is available for download,too.

It runs on any computer with x86 architecture. Just boot from the CD. This life CD is in an early stage of developement, so you might encounter bugs. The Hets-Live-CD is based on Knoppix.

Hets binaries are available here:

• Linux daily snapshot    stable prerelease    latest release    all versions
• (Tiger) Mac daily snapshot   stable prerelease    latest release    all versions
• (Leopard) Intel Mac daily snapshot   stable prerelease    latest release    all versions
• Sparc Solaris daily snapshot   stable prerelease    latest release    all versions
• PC Solaris daily snapshot   stable prerelease    latest release    all versions

How to install Hets:

    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 displaying development graphs (with the -g option), you need to install Tcl/Tk (which probably has been already installed on your computer anyway) and uDraw(Graph) (formerly known as daVinci). 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).
• 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.
• The connection of Hets to other theorem provers is under development