Advertisement

Constructive Formalization of Hybrid Logic with Eventualities

  • Christian Doczkal
  • Gert Smolka
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)

Abstract

This paper reports on the formalization of classical hybrid logic with eventualities in the constructive type theory of the proof assistant Coq. We represent formulas and models and define satisfiability, validity, and equivalence of formulas. The representation yields the classical equivalences and does not require axioms. Our main results are an algorithmic proof of a small model theorem and the computational decidability of satisfiability, validity, and equivalence of formulas. We present our work in three steps: propositional logic, modal logic, and finally hybrid logic.

Keywords

hybrid logic eventualities small model theorem decision procedures Coq Ssreflect 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., et al. (eds.) [2], pp. 821–868Google Scholar
  2. 2.
    Blackburn, P., van Benthem, J., Wolter, F. (eds.): Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3. Elsevier (2007)Google Scholar
  3. 3.
    Caldwell, J.L.: Classical Propositional Decidability Via Nuprl Proof Extraction. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 105–122. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Programming 2(3), 241–266 (1982)CrossRefzbMATHGoogle Scholar
  5. 5.
    Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. System Sci. 30(1), 1–24 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. System Sci., 194–211 (1979)Google Scholar
  7. 7.
    Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A Modular Formalisation of Finite Group Theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 86–101. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  9. 9.
    Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, INRIA (2008), http://hal.inria.fr/inria-00258384/en/
  10. 10.
    Ilik, D., Lee, G., Herbelin, H.: Kripke models for classical logic. Ann. Pure Appl. Logic 161(11), 1367–1378 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Kaminski, M., Schneider, T., Smolka, G.: Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS (LNAI), vol. 6793, pp. 196–210. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  12. 12.
    Kaminski, M., Smolka, G.: Terminating Tableaux for Hybrid Logic with Eventualities. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 240–254. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    Norrish, M.: Mechanised Computability Theory. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 297–311. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  14. 14.
    Pratt, V.R.: Models of program logics. In: Proc. 20th Annual Symp. on Foundations of Computer Science (FOCS 1979), pp. 115–122. IEEE Computer Society Press (1979)Google Scholar
  15. 15.
    The Coq Development Team: The Coq Proof Assistant Reference Manual - Version 8.3. INRIA, France (2011), http://coq.inria.fr
  16. 16.
    Théry, L.: A machine-checked implementation of Buchberger’s algorithm. J. Autom. Reasoning 26(2), 107–137 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Zammit, V.: A Mechanization of Computability Theory in HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 431–446. Springer, Heidelberg (1996)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Christian Doczkal
    • 1
  • Gert Smolka
    • 1
  1. 1.Saarland UniversitySaarbrückenGermany

Personalised recommendations