Abstract
This work presents two provers for basic hybrid logic HL(@), which have been implemented with the aim of comparing the internalised tableau calculi independently proposed, respectively, by Bolander and Blackburn [3] and Cerrito and Cialdea Mayer [5]. Experimental results are reported, evaluating, from the practical point of view, the different treatment of nominal equalities of the two calculi.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Areces, C., Heguiabehere, J.: hGen: A random CNF formula generator for hybrid languages. In: Methods for Modalities 3 (M4M-3), Nancy, France (2003)
Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. Journal of Automated Reasoning 24(3), 297–317 (2000)
Bolander, T., Blackburn, P.: Termination for hybrid tableaus. Journal of Logic and Computation 17(3), 517–554 (2007)
Cerrito, S., Cialdea Mayer, M.: An efficient approach to nominal equalities in hybrid logic tableaux. Journal of Applied Non-classical Logics (to appear)
Cerrito, S., Cialdea Mayer, M.: Terminating tableaux for HL(@) without loop-checking. Technical Report IBISC-RR-2007-07, Ibisc Lab., Université d’Evry Val d’Essonne (2007), http://www.ibisc.univ-evry.fr/Vie/TR/2007/IBISC-RR2007-07_OnlinePDF.pdf
Cerrito, S., Cialdea Mayer, M.: Tableaux with substitution for hybrid logic with the global and converse modalities. Technical Report RT-DIA-155-2009, Dipartimento di Informatica e Automazione, Università di Roma Tre (2009)
Cialdea Mayer, M., Cerrito, S., Benassi, E., Giammarinaro, F., Varani, C.: Two tableau provers for basic hybrid logic. Technical Report RT-DIA-145-2009, Dipartimento di Informatica e Automazione, Università di Roma Tre (2009)
Gent, I.P., Walsh, T.: The SAT phase transition. In: Proceedings of the Eleventh European Conference on Artificial Intelligence, ECAI’94, pp. 105–109 (1994)
Götzmann, D.: Spartacus: A tableau prover for hybrid logic. Master’s thesis, Saarland University (2009)
Götzmann, D., Kaminski, M., Smolka, G.: Spartacus: A tableau prover for hybrid logic. In: M4M6. Computer Science Research Reports, vol. 128, pp. 201–212. Roskilde University (2009)
Hoffmann, G., Areces, C.: HTab: A terminating tableaux system for hybrid logic. Electronic Notes in Theoretical Computer Science, vol. 231, pp. 3–19 (2007); Proceedings of the 5th Workshop on Methods for Modalities, M4M-5 (2007)
Leroy, X.: The Objective Caml system, release 3.11. Documentation and user’s manual (2008), http://caml.inria.fr/
Herod web page (2009), http://cialdea.dia.uniroma3.it/herod/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cialdea Mayer, M., Cerrito, S. (2010). Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-14203-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14202-4
Online ISBN: 978-3-642-14203-1
eBook Packages: Computer ScienceComputer Science (R0)