HTab: a Terminating Tableaux System for Hybrid Logic. Hybrid logic is a formalism that is closely related to both modal logic and description logic. A variety of proof mechanisms for hybrid logic exist, but the only widely available implemented proof system, HyLoRes, is based on the resolution method. An alternative to resolution is the tableaux method, already widely used for both modal and description logics. Tableaux algorithms have also been developed for a number of hybrid logics, and the goal of the present work is to implement one of them. In this article we present the implementation of a terminating tableaux algorithm for the hybrid logic H(@,A)H(@,A). The performance of the tableaux algorithm is compared with the performances of HyLoRes, HyLoTab (a system based on a different tableaux algorithm) and RacerPro. HTab is written in the functional language Haskell, using the Glasgow Haskell Compiler (GHC). The code is released under the GNU GPL and can be downloaded from http://hylo.loria.fr/intohylo/htab.php.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Areces, Carlos; Orbe, Ezequiel: Symmetric blocking (2015)
- Kaminski, Mark; Smolka, Gert: A goal-directed decision procedure for hybrid PDL (2014)
- Madeira, Alexandre; Faria, José M.; Martins, Manuel A.; Barbosa, Luís S.: Hybrid specification of reactive systems: an institutional approach (2011)
- Cerrito, Serenella; Mayer, Marta Cialdea: An efficient approach to nominal equalities in hybrid logic tableaux (2010)
- Cialdea Mayer, Marta; Cerrito, Serenella: Herod and Pilate: two tableau provers for basic hybrid logic (2010)
- Götzmann, Daniel; Kaminski, Mark; Smolka, Gert: Spartacus: a tableau prover for hybrid logic (2010)
- Hoffmann, Guillaume: HTab: a terminating tableaux system for hybrid logic (2009)
- Sustretov, Dmitry; Hoffmann, Guillaume; Areces, Carlos; Blackburn, Patrick: Experiments in theorem proving for topological hybrid logic (2009)