Advertisement

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

  • Marta Cialdea MayerEmail author
Article

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. 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. 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. 3.
    Areces, C., Gorín, D.: Unsorted functional translations. Electron. Notes Theor. Comput. Sci. 278, 3–16 (2011)MathSciNetzbMATHGoogle Scholar
  4. 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. 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. 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. 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. 8.
    Blackburn, P., Seligman, J.: Hybrid languages. J. Log. Lang. Inf. 4, 251–272 (1995)MathSciNetzbMATHGoogle Scholar
  9. 9.
    Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Log. Comput. 17(3), 517–554 (2007)MathSciNetzbMATHGoogle Scholar
  10. 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. 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. 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. 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. 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. 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. 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. 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. 18.
    Donini, F.M., Massacci, F.: EXPTIME tableaux for \(\cal{ALC}\). Artif. Intell. 124(1), 87–138 (2000)zbMATHGoogle Scholar
  19. 19.
    Freeman, J.W.: Hard random 3-SAT problems and the Davis–Putnam procedure. Artif. Intell. 81(1), 183–198 (1996)MathSciNetGoogle Scholar
  20. 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. 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. 22.
    Grädel, E.: On the restraining power of guards. J. Symb. Log. 64, 1719–1742 (1998)MathSciNetzbMATHGoogle Scholar
  23. 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. 24.
    Hoffmann, G.: Tâches de raisonnement en logiques hybrides. PhD thesis, Université Henri Poincaré—Nancy I (2010)Google Scholar
  25. 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. 26.
    Horrocks, I., Glimm, B., Sattler, U.: Hybrid logics and ontology languages. Electron. Notes Theor. Comput. Sci. 174, 3–14 (2007)zbMATHGoogle Scholar
  27. 27.
    Horrocks, I., Patel-Schneider, P.F.: Optimizing description logic subsumption. J. Log. Comput. 9, 267–293 (1999)MathSciNetzbMATHGoogle Scholar
  28. 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. 29.
    Horrocks, I., Sattler, U.: A tableau decision procedure for \(\cal{SHOIQ}\). J. Autom. Reason. 39(3), 249–276 (2007)MathSciNetzbMATHGoogle Scholar
  30. 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. 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. 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. 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. 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. 35.
    Mundhenk, M., Schneider, T.: Undecidability of multi-modal hybrid logics. Electron. Notes Theor. Comput. Sci. 174(6), 29–43 (2007)zbMATHGoogle Scholar
  36. 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. 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. 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. 39.
    Pelletier, F.J.: Seventy-five problems for testing automatic theorem provers. J. Autom. Reason. 2(2), 191–216 (1986)MathSciNetzbMATHGoogle Scholar
  40. 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. 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. 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. 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. 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. 45.
    van Eijck, J.: Constraint tableaux for hybrid logics. CWI, Amsterdam (2002)Google Scholar
  46. 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. 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

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  1. 1.Dipartimento di IngegneriaUniversità degli Studi Roma TreRomeItaly

Personalised recommendations