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.
- general-purpose logics: Propositional, QBF, TPTP/SoftFOL, CASL (FOL), HasCASL (HOL)
- logical frameworks: Isabelle, LF, DFOL
- modeling languages: Meta-Object Facility (MOF), Query/View/Transformation (QVT)
- ontologies and constraint languages: OWL, CommonLogic, RelScheme, ConstraintCASL
- reactive systems: CspCASL, CoCASL, ModalCASL, Maude
- programming languages: Haskell, VSE
- logics of specific tools: Reduce, DMU (CATIA)
- minisat and zChaff, which are SAT solvers,
- SPASS, Vampire, Darwin, Hyper and MathServe, which are automatic first-order theorem provers,
- Pellet and Fact++, description logic tableau provers,
- Leo-II and Satallax, automated higher-order provers,
- Isabelle, an interactive higher-order theorem prover,
- CSPCASL-prover, an Isabelle-based prover for CspCASL,
- VSE, an interactive prover for dynamic logic.
The structuring constructs of the heterogeneous specification language are those of the language CASL, plus some constructs to select languages (logics) and language translations. The heterogeneous specification language of Hets is called HetCASL. However, Hets can also read other structuring constructs, like those of Haskell, Maude or OWL. 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.
You can try out Hets using the Web-based interface
A compressed (1.2G, uncompressed 4.2G) virtual box image can be downloaded from here. username/password is ubuntu/reverse.
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 -s "deb http://ppa.launchpad.net/hets/hets/ubuntu trusty main"
sudo apt-get update
sudo apt-get build-dep hets
These Disk images for the Hets application have only limited functionality. (GTK based menus are missing.)
(these are usually not needed but may replace the binaries from above)
- Linux x86
- Linux x86_64
- Intel Mac (Mavericks)
- Solaris
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 (or "otools -L hets" on Macs) to see which libraries are missing.)
- 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 or 8.5) (which probably has been already installed on your computer anyway). Make sure uDrawGraph and wish are in your $PATH.
Download the CASL libraries and set $HETS_LIB to the folder containing these.
Hets is called with
hets filename
or
hets -g filename
For entering the command line mode, just call
hets -I
For a short description of the options, call
hets --help
A good starting point is the Hets user guide and the Hets user guide for Common Logic users. Furthermore two vidoes showing a heterogeneous proof are available:
For a formal introduction to hets see the introductory paper The Heterogeneous Tool Set by Till Mossakowski, Christian Maeder, Klaus Lüttich and Stefan Wölfl. For more in-depth information about Hets see the thesis Heterogeneous specification and the heterogeneous tool set by Till Mossakowski.
For questions related to hets there is a mailing list.
To support writing CASL specifications we have an emacs mode
With the option "-o pp.tex" hets can produce nice LaTeX output from your specifictions that can be embedded in your publications using the hetcasl.sty style file.
A good starting point is the code documentation for Hets - the Heterogeneous Tool Set.
Since Hets is rather large and complex we recommend following the interactive session in Debugging and Testing Hets to get familiar with the central datastructures of Hets.
The formal background and the general structure of Hets is described in chapter 7 of Heterogeneous specification and the heterogeneous tool set.
Hets is written in Haskell, and is compiled using GHC using a couple of language extensions. Among the Haskell books and tutorials we recommend Real World Haskell. The language definition covers the Haskell98 standard which we are supposed to stick to in most cases. Make sure that you are familiar with at least the most common library functions of the Prelude. For searching or looking up any library functions you may also try Hoogle.
Also look into programming guidelines and things to avoid in Haskell.
Dependencies can be installed as specified in Hets Developtment
Before committing haskell source files you may check compliance to the programming guidelines:
- Use scan which can be installed by
cabal install scan. - The comments in your haskell sources should not cause
haddockto fail. Aftermake(for re-compiling changed sources)make docwill callhaddock. - Also check your source with hlint which you may install by
cabal install hlint.
Also have a look at the current Release Notes and Debugging and Testing Hets.
If you want to participate in the Hets development feel free to tell us via our mailing list for Hets developers. This mailing list can also be read via http://news.gmane.org/gmane.comp.lang.hets.devel.
If you wish to make larger changes we generally recommend forking this repository. You can however request access to this repository if you plan on contributing regularly.
- We recommend the Git - SVN Crash Course.
- For github specific info on checking out this repository see Fetching a remote.
The Hets source code is licensed under the GPLv2 or higher