Try out Hets, using the Web-based interface
The Hets license (English German) is GPL. See at the end of this page how to obtain the sources.
Report a bug or see
the list of known issues on our
The best way to use hets is under Ubuntu. Possibly run this OS in a virtual
A compressed (1.2G, uncompressed 4.2 G) virtual box image can be downloaded from
here. username/password is ubuntu/reverse.
Hets under Ubuntu Precise Pangolin (12.04)
For Ubuntu Raring (13.04) or Saucy (13.10) replace "precise" in the command above.
- the basic system
sudo apt-add-repository ppa:hets/hets
sudo apt-get update
sudo apt-get install hets-core
- additionally, you can install (via apt-get) hets-ontology
- for the full system including all of these, use hets instead of hets-core
- for Hets development, additionally type in:
sudo apt-add-repository "deb http://ppa.launchpad.net/hets/hets/ubuntu precise main"
(or: sudo apt-add-repository -s "deb http://ppa.launchpad.net/hets/hets/ubuntu raring main")
sudo apt-get update
sudo apt-get build-dep hets
Although this includes installation of the Hets sources, it is recommended to use the sources from the subversion repository (see the end of this page).
Hets Images for Mac OS X 10.9 (Mavericks)
Hets binaries are available here:
(these are usually not needed but may replace the binaries from above)
How to use a hets binary?
Just download the binary and put it somewhere in the $PATH.
and set $HETS_LIB to the folder containing these.
- 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 (or "otools -L hets" on Macs) to see which libraries are missing.)
- For displaying development graphs (with the -g option), you need
(formerly known as daVinci) that relies
on Tcl/Tk (version 8.4 or 8.5)
(which probably has been already installed on your computer anyway).
Make sure uDrawGraph and wish are in your $PATH.
How to install software needed for theorem proving with Hets? (only needed when working with the binaries)
- For interactive theorem proving you may install
- For automatic theorem proving you may install
- For reasoning about OWL specifications you may install
and set $PELLET_PATH to the directory containing the script pellet.sh.
Obtaining the Hets sources
Hets is written in Haskell.
You can obtain the Hets sources from the subversion repository with:
svn co https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk Hets
Information for Hets developers