×

zbMATH — the first resource for mathematics

An efficient approach to nominal equalities in hybrid logic tableaux. (English) Zbl 1242.03029
Summary: Basic hybrid logic extends modal logic with the possibility of naming worlds by means of a distinguished class of atoms (called nominals) and the so-called satisfaction operator, that allows one to state that a given formula holds at the world named \(a\), for some nominal \(a\). Hence, in particular, hybrid formulae include “equality” assertions, stating that two nominals are distinct names for the same world. The treatment of such nominal equalities in proof systems for hybrid logics may induce many redundancies. This paper introduces an internalized tableau system for basic hybrid logic, significantly reducing such redundancies. The calculus enjoys a strong termination property: tableau construction terminates without relying on any specific rule application strategy, and no loop-checking is needed. The treatment of nominal equalities specific of the proposed calculus is briefly compared to other approaches. Its practical advantages are demonstrated by empirical results obtained by use of implemented systems. Finally, it is briefly shown how to extend the calculus to include the global and converse modalities.

MSC:
03B35 Mechanization of proofs and logical operations
03B62 Combined logics
68T27 Logic in artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alechina N., Journal of Logic and Computation 13 (6) pp 936– (2003) · Zbl 1093.68032
[2] Areces C., The Journal of Symbolic Logic 66 (3) pp 977– (2001) · Zbl 0984.03018
[3] Areces C., Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, number 1683 in LNCS pp 307–
[4] Areces C., Journal of Logic and Computation 11 (5) pp 717– (2001) · Zbl 0993.03007
[5] Areces C., Proceedings of CADE-18 pp 156–
[6] Areces C., Methods for Modalities 3 (2003)
[7] Balsiger P., Journal of Automated Reasoning 24 (3) pp 297– (2000) · Zbl 0955.03013
[8] DOI: 10.3166/jancl.14.447-475 · Zbl 1185.68290
[9] Blackburn P., Journal of Logic and Computation 10 (1) pp 137– (2000) · Zbl 0953.03018
[10] DOI: 10.1017/CBO9781107050884
[11] Blackburn P., Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2002), number 2381 in LNAI pp 38– (2002)
[12] Bolander T., Journal of Logic and Computation 17 (3) pp 517– (2007) · Zbl 1140.03005
[13] Bolander T., Proceedings of the 5th Workshop on Methods for Modalities, 2007 231 pp 21–
[14] Bolander T., Journal of Logic and Computation 16 (6) pp 737– (2006) · Zbl 1122.03006
[15] Braüner T., Journal of Logic and Computation 14 (3) pp 329– (2004) · Zbl 1060.03036
[16] Cerrito S., Terminating tableaux for HL(@) without loop-checking (2007)
[17] Cerrito S., Tableaux with Substitution for Hybrid Logic with the Global and Converse Modalities (2009)
[18] Cialdea Mayer M., Two tableau provers for basic hybrid logic (2009) · Zbl 1291.68333
[19] Franceschet M., Methods for Modalities 3 pp 109– (2003)
[20] Franceschet M., Proceedings of Computer Science Logic 2005 3634 pp 339–
[21] Götzmann D., Spartacus: A Tableau Prover for Hybrid Logic (2009)
[22] Hoffmann G., Proceedings of the 5th Workshop on Methods for Modalities, 2007 231 pp 3–
[23] DOI: 10.1093/logcom/9.3.385 · Zbl 0940.03039
[24] Horrocks I., Journal of Automated Reasoning 39 (3) pp 249– (2007) · Zbl 1132.68734
[25] Kaminski M., Proc. of IJCAR 2008 5195 pp 210–
[26] Kaminski M., Proceedings of the 5th Workshop on Methods for Modalities, 2007 231 pp 241–
[27] Kaminski M., Journal of Logic, Language and Information 18 (4) pp 437– (2009) · Zbl 1188.03013
[28] Leroy X., The Objective Caml system, release 3.11 (2008)
[29] Tzakova M., Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1999) 1617 pp 278– (1999)
[30] van Eijck J., HyLoTab – Tableau-based theorem proving for hybrid logics (2002)
[31] van Eijck J., Constraint tableaux for hybrid logics (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.