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.

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

Stable version (1.6.2):

• Sources and example formulas

Development version:

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 $HOME/.cabal/bin

See the history.