HTab: A Terminating Tableaux System for Hybrid Logic

G. Hoffmann and C. Areces. HTab: A Terminating Tableaux System for Hybrid Logic. Electronic Notes in Theoretical Computer Science, 231:3–19, Elsevier, 2009. Proceedings of Methods for Modalities 5

Download

[pdf] 

Abstract

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 basic hybrid logic. The performance of the tableaux algorithm is compared with the performances of HyLoRes and HyLoTab (a system based on a different tableaux algorithm). HTab is implemented 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://trac.loria.fr/projects/htab.

BibTeX

@Article{Hoffmann2009,
  author =       "G. Hoffmann and C. Areces",
  journal =      "Electronic Notes in Theoretical Computer Science",
  title =        "{HT}ab: {A} Terminating Tableaux System for Hybrid
                 Logic",
  year =         "2009",
  note =         "Proceedings of Methods for Modalities 5",
  pages =        "3--19",
  volume =       "231",
  abstract =     "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 basic hybrid logic. The performance of the tableaux
                 algorithm is compared with the performances of HyLoRes
                 and HyLoTab (a system based on a different tableaux
                 algorithm). HTab is implemented 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://trac.loria.fr/projects/htab.",
  editor =       "C. Areces and S. Demri",
  owner =        "areces",
  publisher =    "Elsevier",
  timestamp =    "2007.10.25",
}