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  and  for the general tableau algorithm and  for the pattern-based blocking and lazy branching technique currently used.
Download the source code of HTab either using Darcs:
darcs clone --lazy http://hub.darcs.net/gh/htab
Or downloading the source code as a zip file and unpacking it.
Compiling and using
A help is available by running:
 https://cs.famaf.unc.edu.ar/~hoffmann/publi/2009_m4m_htab.pdf  https://cs.famaf.unc.edu.ar/~hoffmann/publi/2010_jal.pdf  http://www.ps.uni-saarland.de/papers/abstracts/GoetzmannKaminskiSmolkaSpartacus.pdf