HyLoBan: A Game Based Prover for Hybrid Logics with Topological Semantics

HyLoBan is a prover for the hybrid logic equipped with nominals and the universal modality, over topological semantic. It can test satisfiability of formulas over topological spaces with the T0 or T1 axiom.

Main Features

  • Guaranteed termination for all formulas of the hybrid logic equipped with nominals and the universal modality, over T0 and T1 topological spaces.

The Implementation

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

Our TODO list includes:

  • Optimizations in the generation of Hintika Sets.

Download

The haskell source can be downloaded from