Otto-von-Guericke-Universität Magdeburg


Hets - the Heterogeneous Tool Set

Obtaining Hets     Documentation     Source code and information for developers

Hets is a parsing, static analysis and proof management tool incorporating various provers and different specification languages, thus providing a tool for heterogeneous specifications. Logic translations are first-class citizens.

Supported languages

The following provers have been connected to Hets:

Hets' input languages for structured and heterogeneous theories:

All these are mapped to so-called development graphs and processed with a proof calculus for heterogeneous development graphs that allows to decompose global proof obligations into local ones (during this, Hets also needs to compute colimits of theories over the involved logics).

Hets is based on a graph of logics and logic translations. The overall architecture is depicted below. Adding new logics and logic translations to Hets can be done with moderate effort by adding some Haskell code to the Hets source. With the Latin project, this becomes much easier: logics (and in the near future also logic translations) can be declaratively specified in LF.



Last Modification: 27.04.2015 - Contact Person: Webmaster