Document Open Access Logo

Verified Decision Procedures for Modal Logics

Authors Minchao Wu , Rajeev Goré

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.31.pdf
  • Filesize: 499 kB
  • 19 pages

Document Identifiers

Author Details

Minchao Wu
  • Research School of Computer Science, Australian National University, Australia
Rajeev Goré
  • Research School of Computer Science, Australian National University, Australia

Cite AsGet BibTex

Minchao Wu and Rajeev Goré. Verified Decision Procedures for Modal Logics. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.31

Abstract

We describe a formalization of modal tableaux with histories for the modal logics K, KT and S4 in Lean. We describe how we formalized the static and transitional rules, the non-trivial termination and the correctness of loop-checks. The formalized tableaux are essentially executable decision procedures with soundness and completeness proved. Termination is also proved in order to define them as functions in Lean. All of these decision procedures return a concrete Kripke model in cases where the input set of formulas is satisfiable, and a proof constructed via the tableau rules witnessing unsatisfiability otherwise. We also describe an extensible formalization of backjumping and its verified implementation for the modal logic K. As far as we know, these are the first verified decision procedures for these modal logics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Software and its engineering → Formal methods
Keywords
  • Formal Methods
  • Interactive Theorem Proving
  • Modal Logic
  • Lean

Metrics

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

Supplementary Materials

References

  1. Samson Abramsky. Domain Theory and the Logic of Observable Properties. CoRR, abs/1112.0347, 2011. URL: http://arxiv.org/abs/1112.0347.
  2. José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesus Martín-Mateos, and José-Luis Ruiz-Reina. A Formally Verified Prover for the ALC Description Logic. In Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'07, pages 135-150, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1792233.1792244.
  3. Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, New York, NY, USA, 2003. Google Scholar
  4. Franz Baader and Bernhard Hollunder. A terminological knowledge representation system with complete inference algorithms. In Harold Boley and Michael M. Richter, editors, Processing Declarative Knowledge, pages 67-86, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. Google Scholar
  5. Peter Balsiger, Alain Heuerding, and Stefan Schwendimann. A Benchmark Method for the Propositional Modal Logics K, KT, S4. Journal of Automated Reasoning, 24(3):297-317, April 2000. URL: https://doi.org/10.1023/A:1006249507577.
  6. Bruno Bentzen. A Henkin-style completeness proof for the modal logic S5, 2019. URL: https://github.com/bbentzen/mpl.
  7. Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. Journal of Automated Reasoning, 61(1):333-365, June 2018. URL: https://doi.org/10.1007/s10817-018-9455-7.
  8. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999. Google Scholar
  9. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378-388, Cham, 2015. Springer International Publishing. Google Scholar
  10. Paulien de Wind. Modal Logic in Coq. Master’s thesis, Vrije Universiteit Amsterdam, 2001. Google Scholar
  11. Christian Doczkal and Joachim Bard. Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 42-52, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3167088.
  12. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. In International Conference on Computer Aided Verification, pages 463-478. Springer, 2013. Google Scholar
  13. Rajeev Goré. Tableau Methods for Modal and Temporal Logics. In Marcello D'Agostino, Dov M. Gabbay, Reiner Hähnle, and Joachim Posegga, editors, Handbook of Tableau Methods, pages 297-396. Springer Netherlands, Dordrecht, 1999. URL: https://doi.org/10.1007/978-94-017-1754-0_6.
  14. Rajeev Goré. AND-OR tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Automated Reasoning, pages 26-45, Cham, 2014. Springer International Publishing. Google Scholar
  15. Rajeev Goré, Kerry Olesen, and Jimmy Thomson. Implementing Tableau Calculi Using BDDs: BDDTab System Description. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Automated Reasoning, pages 337-343, Cham, 2014. Springer International Publishing. Google Scholar
  16. Alain Heuerding, Michael Seyfried, and Heinrich Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, pages 210-225, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. Google Scholar
  17. M. J. Hidalgo-Doblado, J. A. Alonso-Jiménez, J. Borrego-Díaz, F. J. Martín-Mateos, and J. L. Ruiz-Reina. Formally Verified Tableau-Based Reasoners for a Description Logic. Journal of Automated Reasoning, 52(3):331-360, March 2014. URL: https://doi.org/10.1007/s10817-013-9291-8.
  18. Simon Jantsch and Michael Norrish. Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving, pages 306-323, Cham, 2018. Springer International Publishing. Google Scholar
  19. Mark Kaminski, Thomas Schneider, and Gert Smolka. Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics. In Kai Brünnler and George Metcalfe, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 196-210, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  20. Mark Kaminski and Tobias Tebbi. InKreSAT: Modal reasoning via incremental reduction to SAT. In Maria Paola Bonacina, editor, CADE-24, volume 7898 of LNCS, pages 436-442. Springer, June 2013. Google Scholar
  21. LudvikGalois. A verfied tableau prover for classical propositional logic, 2018. URL: https://github.com/LudvikGalois/coq-CPL-NNF-tableau.
  22. J. C. C. McKinsey and Alfred Tarski. The Algebra of Topology. Annals of Mathematics, 45(1):141-191, 1944. URL: http://www.jstor.org/stable/1969080.
  23. John CC McKinsey and Alfred Tarski. Some theorems about the sentential calculi of Lewis and Heyting. The journal of symbolic logic, 13(1):1-15, 1948. Google Scholar
  24. John-Jules Ch Meyer and Wiebe Van Der Hoek. Epistemic Logic for AI and Computer Science. Cambridge University Press, New York, NY, USA, 1995. Google Scholar
  25. Alexander Schimpf, Stephan Merz, and Jan-Georg Smaus. Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. In TPHOLs, 2009. Google Scholar
  26. Anders Schlichtkrull. Formalization of the Resolution Calculus for First-Order Logic. Journal of Automated Reasoning, 61(1):455-484, June 2018. URL: https://doi.org/10.1007/s10817-017-9447-z.
  27. Dmitry Tsarkov and Ian Horrocks. Ordering Heuristics for Description Logic Reasoning. In Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI'05, pages 609-614, San Francisco, CA, USA, 2005. Morgan Kaufmann Publishers Inc. URL: http://dl.acm.org/citation.cfm?id=1642293.1642391.
  28. Dmitry Tsarkov and Ian Horrocks. FaCT++ description logic reasoner: System description. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, pages 292-297, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  29. Florian Widmann. Tableaux-based Decision Procedures for Fixed Point Logics. PhD thesis, Australian National University, 2010. Google Scholar
  30. Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, and Koichi Takahashi. Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic. In Proceedings of the 2Nd International Conference on Verified Software: Theories, Tools, Experiments, VSTTE '08, pages 115-129, Berlin, Heidelberg, 2008. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-87873-5_12.
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