Hets: Languages and tools supported by Hets
| Syntax for invoking the language |
Parser |
static Analysis |
Proof support |
|
| CASL |
logic CASL |
x |
x |
(x) |
| CoCASL |
logic CoCASL |
x |
(x) |
(x) |
| ModalCASL |
logic Modal |
x |
x |
(x) |
| HasCASL |
logic HasCASL |
x |
(x) |
(x) |
| Haskell |
logic Haskell |
x |
x |
|
| CSP-CASL |
logic CspCASL |
(x) |
||
| OWL-DL |
logic OWL_DL |
x |
(x) |
|
| CASL_DL |
logic CASL_DL |
x |
The following provers have been connected to Hets:
- Isabelle, an interactive higher-order theorem prover,
- SPASS, an automatic first-order theorem prover.
- The connection of Hets to other theorem provers is under development
Author: Dr. Till Mossakowski
| Last updated: July 13, 2007 |  |