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.

HTab is implemented in Haskell, and the executable is generated using the Glasgow Haskell Compiler.

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.

• System Description.
• User Manual.

The haskell source can be downloaded from