×

A prover dealing with nominals, binders, transitivity and relation hierarchies. (English) Zbl 1468.68285

Summary: This work describes the Sibyl prover, an implementation of a tableau based proof procedure for multi-modal hybrid logic with the converse, graded and global modalities, and enriched with features largely used in description logics: transitivity and relation hierarchies. The proof procedure is provably terminating when the input problem belongs to an expressive decidable fragment of hybrid logic. After a description of the implemented proof procedure, the way how the implementation deals with the most delicate aspects of the calculus is explained. Some experimental results, run on sets of randomly generated problems as well as some hand-tailored ones, show only a moderate deterioration in the performances of the prover when the number of transitivity and inclusion axioms increase. Sibyl is compared with other provers (HTab, the hybrid logic prover whose expressive power is closer to Sibyl’s one, and the first-order prover SPASS). The obtained results show that Sibyl has reasonable performances.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodriguez-Artalejo, M. (eds.) Computer Science Logic, pp. 307-321. Springer (1999) · Zbl 0942.03048
[2] Areces, C., Gennari, R., Heguiabere, J., de Rijke, M.: Tree-based heuristics in modal theorem proving. In: Proceedings of the 14th European Conference on Artificial Intelligence (ECAI 2000), pp. 199-203 (2000)
[3] Areces, C.; Gorín, D., Unsorted functional translations, Electron. Notes Theor. Comput. Sci., 278, 3-16 (2011) · Zbl 1347.03037 · doi:10.1016/j.entcs.2011.10.002
[4] Areces, Carlos; Heguiabehere, Juan, HyLoRes 1.0: Direct Resolution for Hybrid Logics, Automated Deduction—CADE-18, 156-160 (2002), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1072.68560
[5] Areces, C., Heguiabehere, J.: hGen: A random CNF formula generator for hybrid languages. In: Proceedings of the 3rd Workshop on Methods for Modalities (M4M-3), Nancy, France (2003)
[6] Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logics, pp. 821-868. Elsevier (2007) · Zbl 1114.03001
[7] Balsiger, P.; Heuerding, A.; Schwendimann, S., A benchmark method for the propositional modal logics K, KT, S4, J. Autom. Reason., 24, 3, 297-317 (2000) · Zbl 0955.03013 · doi:10.1023/A:1006249507577
[8] Blackburn, P.; Seligman, J., Hybrid languages, J. Log. Lang. Inf., 4, 251-272 (1995) · Zbl 0847.03009 · doi:10.1007/BF01049415
[9] Bolander, T.; Blackburn, P., Termination for hybrid tableaus, J. Log. Comput., 17, 3, 517-554 (2007) · Zbl 1140.03005 · doi:10.1093/logcom/exm014
[10] Cerrito, S.; Cialdea Mayer, M., An efficient approach to nominal equalities in hybrid logic tableaux, J. Appl. Non-class. Log., 1-2, 20, 39-61 (2010) · Zbl 1242.03029 · doi:10.3166/jancl.20.39-61
[11] Cerrito, S., Cialdea Mayer, M.: Nominal substitution at work with the global and converse modalities. In: Beklemishev, L., Goranko, V., Shehtman, V. (eds.) Advances in Modal Logic, vol. 8, pp. 57-74. College Publications (2010) · Zbl 1254.03030
[12] Cerrito, S., Cialdea Mayer, M.: A tableaux based decision procedure for a broad class of hybrid formulae with binders. In: Automated Resoning with Analytic Tableaux and Related Methods (TABLEAUX 2011), vol. 6793 of LNAI, pp. 104-118. Springer (2011) · Zbl 1331.68200
[13] Cerrito, S.; Cialdea Mayer, M., A tableau based decision procedure for a fragment of hybrid logic with binders, converse and global modalities, J. Autom. Reason., 51, 2, 197-239 (2013) · Zbl 1314.03018 · doi:10.1007/s10817-012-9257-2
[14] Cialdea Mayer, M.: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies. In: Proceedings of the 24th Conference on Automated Deduction (CADE-24), Number 7898 in LNCS, pp. 76-90. Springer (2013) · Zbl 1381.03018
[15] Cialdea Mayer, M.: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies (extended version). Technical report. arXiv:1312.2894 (2013) · Zbl 1381.03018
[16] Cialdea Mayer, M., Extended decision procedure for a fragment of HL with binders, J. Autom. Reason., 53, 3, 305-315 (2014) · Zbl 1314.03025 · doi:10.1007/s10817-014-9307-z
[17] Cialdea Mayer, M., Cerrito, S.: Herod and Pilate: two tableau provers for basic hybrid logic. In: Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), pp. 255-262. Springer (2010) · Zbl 1291.68333
[18] Donini, Fm; Massacci, F., EXPTIME tableaux for \(\cal{ALC} \), Artif. Intell., 124, 1, 87-138 (2000) · Zbl 0952.68136 · doi:10.1016/S0004-3702(00)00070-9
[19] Freeman, Jw, Hard random 3-SAT problems and the Davis-Putnam procedure, Artif. Intell., 81, 1, 183-198 (1996) · Zbl 1508.68131 · doi:10.1016/0004-3702(95)00051-8
[20] 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)
[21] Götzmann, D., Kaminski, M., Smolka, G.: Spartacus: a tableau prover for hybrid logic. Electron. Notes Theor. Comput. Sci. 262, 127-139 (2010). Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)
[22] Grädel, E., On the restraining power of guards, J. Symb. Log., 64, 1719-1742 (1998) · Zbl 0958.03027 · doi:10.2307/2586808
[23] Hladik, J.: Implementation and evaluation of a tableau algorithm for the guarded fragment. In: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2002), pp. 145-159. Springer (2002) · Zbl 1015.03011
[24] Hoffmann, G.: Tâches de raisonnement en logiques hybrides. PhD thesis, Université Henri Poincaré—Nancy I (2010)
[25] Hoffmann, G., Areces, C.: HTab: A terminating tableaux system for hybrid logic. Electron. Notes Theor. Comput. Sci. 231, 3-19 (2007). Proceedings of the 5th Workshop on Methods for Modalities (M4M-5)
[26] Horrocks, I.; Glimm, B.; Sattler, U., Hybrid logics and ontology languages, Electron. Notes Theor. Comput. Sci., 174, 3-14 (2007) · Zbl 1278.68287 · doi:10.1016/j.entcs.2006.11.022
[27] Horrocks, I.; Patel-Schneider, Pf, Optimizing description logic subsumption, J. Log. Comput., 9, 267-293 (1999) · Zbl 0940.03038 · doi:10.1093/logcom/9.3.267
[28] Horrocks, I.; Sattler, U., A description logic with transitive and inverse roles and role hierarchies, J. Log. Comput., 9, 3, 385-410 (1999) · Zbl 0940.03039 · doi:10.1093/logcom/9.3.385
[29] Horrocks, I.; Sattler, U., A tableau decision procedure for \(\cal{SHOIQ} \), J. Autom. Reason., 39, 3, 249-276 (2007) · Zbl 1132.68734 · doi:10.1007/s10817-007-9079-9
[30] Hustadt, Ullrich; Schmidt, Renate A., Simplification and Backjumping in Modal Tableau, Lecture Notes in Computer Science, 187-201 (1998), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0909.03014
[31] Kaminski, M.; Schneider, S.; Smolka, G., Terminating tableaux for graded hybrid logic with global modalities and role hierarchies, Log. Methods Comput. Sci., 7, 1, 1-21 (2011) · Zbl 1218.03009 · doi:10.2168/LMCS-7(1:5)2011
[32] Kaminski, M., Smolka, G.: Hybrid tableaux for the difference modality. Electron. Notes Theor. Comput. Sci. 231, 241-257 (2007). Proceedings of the 5th Workshop on Methods for Modalities (M4M-5) · Zbl 1347.03044
[33] Kaminski, M.; Smolka, G., Terminating tableau systems for hybrid logic with difference and converse, J. Log. Lang. Inf., 18, 4, 437-464 (2009) · Zbl 1188.03013 · doi:10.1007/s10849-009-9087-8
[34] Marx, M.: Narcissists, stepmothers and spies. In: Proceedings of the 2002 International Workshop on Description Logics (DL 2002). CEUR Workshop Proceedings, Vol. 53 (2002)
[35] Mundhenk, M.; Schneider, T., Undecidability of multi-modal hybrid logics, Electron. Notes Theor. Comput. Sci., 174, 6, 29-43 (2007) · Zbl 1278.03047 · doi:10.1016/j.entcs.2006.11.024
[36] Mundhenk, M.; Schneider, T.; Schwentick, T.; Weber, V., Complexity of hybrid logics over transitive frames, J. Appl. Log., 8, 4, 422-440 (2010) · Zbl 1215.03035 · doi:10.1016/j.jal.2010.08.004
[37] Nalon, C., Hustadt, U., Dixon, C.: KSP: A resolution-based prover for multimodal K, Abridged Report. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, pp. 4919-4923 (2017)
[38] Ohlbach, H.; Schmidt, R., Functional translation and second-order frame properties of modal logics, J. Log. Comput., 7, 5, 581-603 (1997) · Zbl 0976.03019 · doi:10.1093/logcom/7.5.581
[39] Pelletier, Fj, Seventy-five problems for testing automatic theorem provers, J. Autom. Reason., 2, 2, 191-216 (1986) · Zbl 0642.68147 · doi:10.1007/BF02432151
[40] Schild, K.: A correspondence theory for terminological logics: preliminary report. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), pp. 466-471 (1991) · Zbl 0742.68059
[41] Schmidt, Renate A.; Hustadt, Ullrich, A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae, Automated Deduction - CADE-19, 412-426 (2003), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1278.03031
[42] Sutcliffe, G., The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, J. Autom. Reason., 59, 4, 483-502 (2017) · Zbl 1425.68381 · doi:10.1007/s10817-017-9407-7
[43] ten Cate, B., Franceschet, M.: On the complexity of hybrid logics with binders. In: Proceedings of Computer Science Logic, pp. 339-354. Springer (2005) · Zbl 1136.03311
[44] Tsarkov, D.; Horrocks, I.; Patel-Schneider, Pf, Optimizing terminological reasoning for expressive description logics, J. Autom. Reason., 39, 3, 277-316 (2007) · Zbl 1132.68742 · doi:10.1007/s10817-007-9077-y
[45] Van Eijck, J., Constraint tableaux for hybrid logics (2002), Amsterdam: CWI, Amsterdam
[46] van Eijck, J.: HyLoTab—Tableau-based theorem proving for hybrid logics. Manuscript, CWI, Amsterdam. available at https://homepages.cwi.nl/ jve/hylotab/Hylotab.pdf (2002)
[47] Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Proceedings of the 22nd International Conference on Automated Deduction (CADE-22), pp. 140-145. Springer (2009)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.