HTab: A Tableaux Based Theorem Prover for Hybrid Logics
HTab is a libre prover for hybrid logics that uses the tableaux method.
- Handles the basic modal logic K, with nominals, the satisfaction operator @, the universal modality E, role inclusion, and the down-arrow binder ↓.
- Model building.
- Satisfiability, validity and instance retrieval tasks.
Building from the source and installing
You need to have the Haskell Platform installed on your system. Go in the directory containing the file htab.cabal and do:
The binary will be located in
See the history.