The first systems able to handle hybrid logics are being developed right now!!!!


A preliminary prototype of the prover HyLoRes for hybrid logics, based on labeled resolution is being developed by Carlos Areces (LORIA, France), Daniel Gorin (UBA, Argentina) and Juan Heguiabehere (FI, Argentina).

More details available at the HyloRes Web Site.

Hybrid Logics model Checker

This is a C implementation of model checking algorithms for Hybrid Logics MCLite and MCFull being developed by Luigi Dragone.

The model checker requires an Kripke structure for hybrid logics expressed as an XML file and a formula, it checks in which worlds, if any, of the provided model the formula holds.

More details available at the Model checker's web page.