HTab: A Tableaux Based Theorem Prover for Hybrid Logics

HTab is a libre prover for hybrid logics that uses the tableaux method.

Main Features

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

The Implementation

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

Download

Stable version (1.6.2):

Development version:

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:

cabal update
cabal install

The binary will be located in $HOME/.cabal/bin

History

See the history.