zbMATH — the first resource for mathematics

HTab: a terminating tableaux system for hybrid logic. (English) Zbl 1347.68301
Areces, Carlos (ed.) et al., Proceedings of the 5th workshop on methods for modalities (M4M5 2007), Cachan, France, November 29–30, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 231, 3-19 (2009).
Summary: 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 \(\mathcal{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).
For the entire collection see [Zbl 1279.03015].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)
03B62 Combined logics
68N18 Functional programming and lambda calculus
68T27 Logic in artificial intelligence
Full Text: DOI
[1] Areces, C.; Blackburn, P.; Marx, M., A road-map on complexity for hybrid logics, (), 307-321, Proceedings of the 8th Annual Conference of the EACSL, Madrid, September 1999 · Zbl 0942.03048
[2] Areces, C.; Gorín, D., Ordered resolution with selection for H(@), (), 125-141 · Zbl 1108.03304
[3] T. Bolander and P. Blackburn. Decidable tableau calculi for modal and temporal hybrid logics extending K, 2007. Proceedings of Method for Modalities 5, 2007
[4] Bolander, T.; Blackburn, P., Termination for hybrid tableaus, Journal of logic and computation, 17, 517-554, (2007) · Zbl 1140.03005
[5] Cormen, T.H.; Leiserson, C.E.; Rivest, R.L.; Stein, C., Introduction to algorithms, (2001), The MIT Press · Zbl 1047.68161
[6] GHC, The Glasgow Haskell Compiler. http://www.haskell.org/ghc/. Last visited: 15/09/07
[7] Haarslev, V.; Möller, R., RACER system description, Lecture notes in computer science, 2083, 701-705, (2001) · Zbl 0988.68599
[8] Hemaspaandra, Edith, The price of universality, Notre dame journal of formal logic, 37, 2, 174-203, (1996) · Zbl 0865.03032
[9] Horrocks, I.; Patel-Schneider, P., Optimising description logic subsumption, (1998) · Zbl 0910.68204
[10] S. Peyton Jones and J. Hughes (editors). Haskell 98: A non-strict, purely functional language. Technical report, Haskell.org, 1999
[11] Edith Spaan. Complexity of Modal Logics. PhD thesis, Department of Mathematics and Computer Science, University of Amsterdam, 1993 · Zbl 0831.03005
[12] J. van Eijck. HyLoTab — Tableau-based theorem proving for hybrid logics. manuscript, CWI, available from http://www.cwi.nl/ jve/hylotab, 2002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.