HTab, a hybrid logic tableau prover

HTab is a tableau-based satisfiability checker. It currently handles the hybrid logic H(:,E) with role inclusions, and terminates on all inputs.

Relevant references for HTab are [1] and [2] for the general tableau algorithm and [3] for the pattern-based blocking and lazy branching technique currently used.


Download the source code of HTab either using Darcs:

darcs clone --lazy

Or downloading the source code as a zip file and unpacking it.

Compiling and using

To build HTab, you will need at least GHC 7.10, and either cabal-install or stack. Dependencies, including hylolib, will be downloaded and compiled automatically.

A help is available by running:

htab --help

[1] [2] [3]