{:toc}
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, 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.
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 sing the Web-based interface
A compressed (1.2G, uncompressed 4.2 G) 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
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
- (Mavericks) Intel Mac
- Solaris
How do I, as a developer, start working on the project?
- What dependencies does it have (where are they expressed) and how do I install them?
- How can I see the project working before I change anything?
How do I run the project's automated tests?
rake spec
- Run other local services / provide credentials for external services.
rake spec:integration
- Required heroku addons, packages, or chef recipes.
- Required environment variables or credentials not included in git.
- Monitoring services and logging.
Examples of common tasks
e.g.
- How to make curl requests while authenticated via oauth.
- How to monitor background jobs.
- How to run the app through a proxy.
- Internal git workflow
- Pull request guidelines
- Tracker project
- Google group
- irc channel
- "Please open github issues"