# A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies

## Abstract

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.

## Keywords

Automated proof systems Tableaux Modal logic Hybrid logic## Notes

### Acknowledgements

The present version of the Sibyl prover extends and improves the work done by some students in their bachelor or master projects. Beyond them, the author wishes to thank Renate Schmidt for her ready answers to my questions on the SPASS prover and translation issues.

## 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)Google Scholar
- 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)Google Scholar
- 3.Areces, C., Gorín, D.: Unsorted functional translations. Electron. Notes Theor. Comput. Sci.
**278**, 3–16 (2011)MathSciNetzbMATHGoogle Scholar - 4.Areces, C., Heguiabehere, J.: Hylores 1.0: Direct resolution for hybrid logics. In: Proceedings of the 18th International Conference on Automated Deduction (CADE-18), pp. 156–160 (2002). Previously presented in the Proceedings of Methods for Modalities 2 (2001)Google Scholar
- 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)Google Scholar
- 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)Google Scholar
- 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)MathSciNetzbMATHGoogle Scholar - 8.Blackburn, P., Seligman, J.: Hybrid languages. J. Log. Lang. Inf.
**4**, 251–272 (1995)MathSciNetzbMATHGoogle Scholar - 9.Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Log. Comput.
**17**(3), 517–554 (2007)MathSciNetzbMATHGoogle Scholar - 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)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar
- 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)Google Scholar
- 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)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar
- 15.Cialdea Mayer, M.: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies (extended version). Technical report. arXiv:1312.2894 (2013)
- 16.Cialdea Mayer, M.: Extended decision procedure for a fragment of HL with binders. J. Autom. Reason.
**53**(3), 305–315 (2014)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar
- 18.Donini, F.M., Massacci, F.: EXPTIME tableaux for \(\cal{ALC}\). Artif. Intell.
**124**(1), 87–138 (2000)zbMATHGoogle Scholar - 19.Freeman, J.W.: Hard random 3-SAT problems and the Davis–Putnam procedure. Artif. Intell.
**81**(1), 183–198 (1996)MathSciNetGoogle Scholar - 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)Google Scholar
- 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)Google Scholar - 22.Grädel, E.: On the restraining power of guards. J. Symb. Log.
**64**, 1719–1742 (1998)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar
- 24.Hoffmann, G.: Tâches de raisonnement en logiques hybrides. PhD thesis, Université Henri Poincaré—Nancy I (2010)Google Scholar
- 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)Google Scholar - 26.Horrocks, I., Glimm, B., Sattler, U.: Hybrid logics and ontology languages. Electron. Notes Theor. Comput. Sci.
**174**, 3–14 (2007)zbMATHGoogle Scholar - 27.Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. J. Log. Comput.
**9**, 267–293 (1999)MathSciNetzbMATHGoogle Scholar - 28.Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput.
**9**(3), 385–410 (1999)MathSciNetzbMATHGoogle Scholar - 29.Horrocks, I., Sattler, U.: A tableau decision procedure for \(\cal{SHOIQ}\). J. Autom. Reason.
**39**(3), 249–276 (2007)MathSciNetzbMATHGoogle Scholar - 30.Hustadt, U., Schmidt, R.A.: Simplification and backjumping in modaltableau. In: Automated Reasoning with Analytic Tableaux and RelatedMethods. TABLEAUX 1998, pp. 187–201. Springer, Berlin, Heidelberg (1998)Google Scholar
- 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)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar - 33.Kaminski, M., Smolka, G.: Terminating tableau systems for hybrid logic with difference and converse. J. Log. Lang. Inf.
**18**(4), 437–464 (2009)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar
- 35.Mundhenk, M., Schneider, T.: Undecidability of multi-modal hybrid logics. Electron. Notes Theor. Comput. Sci.
**174**(6), 29–43 (2007)zbMATHGoogle Scholar - 36.Mundhenk, M., Schneider, T., Schwentick, T., Weber, V.: Complexity of hybrid logics over transitive frames. J. Appl. Log.
**8**(4), 422–440 (2010)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar
- 38.Ohlbach, H., Schmidt, R.: Functional translation and second-order frame properties of modal logics. J. Log. Comput.
**7**(5), 581–603 (1997)MathSciNetzbMATHGoogle Scholar - 39.Pelletier, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reason.
**2**(2), 191–216 (1986)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar
- 41.Schmidt, R.A., Hustadt, U.: A principle for incorporating axioms into the first-order translation of modal formulae. In: Proceedings of the 19th International Conference on Automated Deduction (CADE-19), pp. 412–426 (2003)Google Scholar
- 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)MathSciNetzbMATHGoogle Scholar - 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)Google Scholar
- 44.Tsarkov, D., Horrocks, I., Patel-Schneider, P.F.: Optimizing terminological reasoning for expressive description logics. J. Autom. Reason.
**39**(3), 277–316 (2007)MathSciNetzbMATHGoogle Scholar - 45.van Eijck, J.: Constraint tableaux for hybrid logics. CWI, Amsterdam (2002)Google Scholar
- 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)Google Scholar