HTab: A Tableaux Based Theorem Prover for Hybrid Logics

HTab is a tableaux prover for hybrid logics.

Main Features

  • 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.

The Implementation

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.


The haskell source can be downloaded from