Document Open Access Logo

Synthetic Completeness for a Terminating Seligman-Style Tableau System

Author Asta Halkjær From

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2020.5.pdf
  • Filesize: 0.79 MB
  • 17 pages

Document Identifiers

Author Details

Asta Halkjær From
  • Technical University of Denmark, Kongens Lyngby, Denmark

Acknowledgements

We thank Patrick Blackburn, Thomas Bolander, Torben Braüner, Klaus Frovin Jørgensen and Jørgen Villadsen for discussions and Lars Hupel, Jasmin Blanchette and the anonymous reviewers for comments on the paper.

Cite AsGet BibTex

Asta Halkjær From. Synthetic Completeness for a Terminating Seligman-Style Tableau System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TYPES.2020.5

Abstract

Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Hybrid logic
  • Seligman-style tableau
  • synthetic completeness
  • Isabelle/HOL

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Carlos Areces, Patrick Blackburn, and Maarten Marx. Hybrid logics: Characterization, interpolation and complexity. The Journal of Symbolic Logic, 66(3):977-1010, 2001. Google Scholar
  2. Stefan Berghofer. First-Order Logic According to Fitting. Archive of Formal Proofs, 2007. , Formal proof development. URL: http://isa-afp.org/entries/FOL-Fitting.html.
  3. Patrick Blackburn. Representation, reasoning, and relational structures: A hybrid logic manifesto. Logic Journal of the IGPL, 8(3):339-365, 2000. Google Scholar
  4. Patrick Blackburn, Thomas Bolander, Torben Braüner, and Klaus Frovin Jørgensen. Completeness and termination for a Seligman-style tableau system. Journal of Logic and Computation, 27(1):81-107, 2017. Google Scholar
  5. Patrick Blackburn and Miroslava Tzakova. Hybridizing concept languages. Annals of Mathematics and Artificial Intelligence, 24(1-4):23-49, 1998. Google Scholar
  6. Jasmin Christian Blanchette. Formalizing the metatheory of logical calculi and automatic provers in isabelle/hol (invited talk). In Assia Mahboubi and Magnus O. Myreen, editors, Certified Programs and Proofs, CPP. Proceedings, pages 1-13. ACM, 2019. Google Scholar
  7. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Abstract completeness. Archive of Formal Proofs, 2014. , Formal proof development. URL: https://isa-afp.org/entries/Abstract_Completeness.html.
  8. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning, 58(1):149-179, 2017. Google Scholar
  9. Thomas Bolander and Patrick Blackburn. Termination for Hybrid Tableaus. Journal of Logic and Computation, 17(3):517-554, 2007. Google Scholar
  10. Thomas Bolander and Torben Braüner. Tableau-based decision procedures for hybrid logic. Journal of Logic and Computation, 16(6):737-763, 2006. Google Scholar
  11. Torben Braüner and Valeria de Paiva. Intuitionistic hybrid logic. Journal of Applied Logic, 4(3):231-255, 2006. Google Scholar
  12. Christian Doczkal and Gert Smolka. Constructive formalization of hybrid logic with eventualities. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, CPP. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 5-20. Springer, 2011. Google Scholar
  13. Melvin Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169. Springer Science & Business Media, 1983. Google Scholar
  14. Asta Halkjær From, Patrick Blackburn, and Jørgen Villadsen. Formalizing a Seligman-style tableau system for hybrid logic. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 474-481, Cham, 2020. Springer International Publishing. Google Scholar
  15. Asta Halkjær From. Epistemic Logic. Archive of Formal Proofs, 2018. , Formal proof development. URL: http://isa-afp.org/entries/Epistemic_Logic.html.
  16. Asta Halkjær From. A sequent calculus for first-order logic. Archive of Formal Proofs, 2019. , Formal proof development. URL: http://isa-afp.org/entries/FOL_Seq_Calc1.html.
  17. Asta Halkjær From. Hybrid Logic. Master’s thesis, Technical University of Denmark, 2020. Google Scholar
  18. Asta Halkjær From. Hybrid logic in the Isabelle proof assistant: Benefits, challenges and the road ahead. In Nicola Olivetti and Rineke Verbrugge, editors, Short Papers: Advances in Modal Logic (AiML) 2020, pages 23-27, 2020. Google Scholar
  19. Didier Galmiche and Yakoub Salhi. Sequent calculi and decidability for intuitionistic hybrid logic. Information and Computation, 209(12):1447-1463, 2011. Google Scholar
  20. Limin Jia and David Walker. Modal proofs as distributed programs (extended abstract). In David A. Schmidt, editor, Programming Languages and Systems, ESOP, Proceedings, volume 2986 of Lecture Notes in Computer Science, pages 219-233. Springer, 2004. Google Scholar
  21. Klaus Frovin Jørgensen, Patrick Blackburn, Thomas Bolander, and Torben Braüner. Synthetic completeness proofs for Seligman-style tableau systems. In Advances in Modal Logic, Volume 11, pages 302-321, 2016. Google Scholar
  22. Sven Linker. Hybrid Multi-Lane Spatial Logic. Archive of Formal Proofs, 2017. , Formal proof. URL: http://isa-afp.org/entries/Hybrid_Multi_Lane_Spatial_Logic.html.
  23. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  24. Jeremy Seligman, Fenrong Liu, and Patrick Girard. Facebook and the epistemic logic of friendship. In Burkhard C. Schipper, editor, Proceedings of the 14th Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2013), pages 229-238, Chennai, India, 2013. Google Scholar
  25. Jerry Seligman. Internalization: The case of hybrid logics. Journal of Logic and Computation, 11(5):671-689, 2001. Google Scholar
  26. Raymond M Smullyan. First-Order Logic. Dover Publications, 1995. Google Scholar
  27. Makarius Wenzel. Isabelle/Isar - a generic framework for human-readable proof documents. From Insight to Proof - Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, 10(23):277-298, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact