HTab: A Tableaux Based Theorem Prover for Hybrid Logics
HTab is a tableaux prover for hybrid logics.
- Guaranteed termination for all inputs of the hybrid logic H(@,E,D), that is the basic modal logic K, nominals, the satisfaction operator @, the universal modality E and the difference modality D.
- Simple model building.
Our TODO list includes:
- Adding classic description logic optimisations.
- Handling frame conditions like transitivity or reflexivity.
- Taking advantage of parallel computing for multicore systems and clusters.
The haskell source can be downloaded from