## Textanfang

### 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

- 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)

## The following provers have been connected to Hets:

- minisat and zChaff, which are SAT solvers,
- SPASS, Vampire, Darwin, KRHyper 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.

## Hets' input languages for structured and heterogeneous theories:

- CASL
- HetCASL
- DOL
- structuring constructs of individual languages, 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.

Last Modification: 27.04.2015 - Contact Person:

Webmaster