Document Open Access Logo

Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL

Authors Asta Halkjær From , Frederik Krogsdal Jacobsen

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.13.pdf
  • Filesize: 0.72 MB
  • 22 pages

Document Identifiers

Author Details

Asta Halkjær From
  • DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark
Frederik Krogsdal Jacobsen
  • DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark

Acknowledgements

We would like to thank Agnes Moesgård Eschen, Alexander Birch Jensen, Anders Schlichtkrull, Simon Tobias Lund and Jørgen Villadsen for comments on drafts. We are very grateful to the anonymous reviewers for their thoughtful comments.

Cite AsGet BibTex

Asta Halkjær From and Frederik Krogsdal Jacobsen. Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.13

Abstract

We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search procedure is based on sequent calculus and we formally verify its soundness and completeness in Isabelle/HOL using an existing abstract framework for coinductive proof trees. Our analytic completeness proof covers both open and closed formulas. Since our deterministic prover considers only the subset of terms relevant to proving a given sequent, we do so as well when building a countermodel from a failed proof. Finally, we formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover can generate human-readable SeCaV proofs which are also machine-verifiable proof certificates.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Proof theory
  • Theory of computation → Program verification
Keywords
  • Isabelle/HOL
  • SeCaV
  • First-Order Logic
  • Prover
  • Soundness
  • Completeness

Metrics

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

Supplementary Materials

References

  1. Clemens Ballarin. Locales: A module system for mathematical theories. Journal of Automated Reasoning, 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  2. Mordechai Ben-Ari. Mathematical Logic for Computer Science. Springer London, 2012. URL: https://doi.org/10.1007/978-1-4471-4129-7.
  3. A. Bentkamp, J. Blanchette, S. Tourret, and P. Vukmirović. Superposition for Full Higher-order Logic. In A. Platzer and G. Sutcliffe, editors, Proceedings of the 28th International Conference on Automated Deduction, number 12699 in Lecture Notes in Computer Science, pages 396-412. Springer-Verlag, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_23.
  4. Stefan Berghofer. First-order logic according to Fitting. Archive of Formal Proofs, August 2007. Formal proof development. URL: https://isa-afp.org/entries/FOL-Fitting.html.
  5. 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, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 1-13. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294087.
  6. 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-4):333-365, 2018. URL: https://doi.org/10.1007/s10817-018-9455-7.
  7. Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. Bindings as bounded natural functors. Proc. ACM Program. Lang., 3(POPL):22:1-22:34, 2019. URL: https://doi.org/10.1145/3290335.
  8. Jasmin Christian Blanchette and Andrei Popescu. Mechanizing the metatheory of Sledgehammer. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Frontiers of Combining Systems, pages 245-260, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-40885-4_17.
  9. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Abstract completeness. Archive of Formal Proofs, April 2014. Formal proof development. URL: https://isa-afp.org/entries/Abstract_Completeness.html.
  10. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Unified classical logic completeness. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, Automated Reasoning, pages 46-60, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-08587-6_4.
  11. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning, 58:149-179, 2017. URL: https://doi.org/10.1007/s10817-016-9391-3.
  12. Joachim Breitner. Visual theorem proving with the Incredible Proof Machine. In J. Blanchette and S. Merz, editors, Interactive Theorem Proving, volume ITP 2016. Springer, Cham, 2016. URL: https://doi.org/10.1007/978-3-319-43144-4_8.
  13. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  14. Mathias Fleury. Optimizing a verified SAT solver. In Julia M. Badger and Kristin Yvonne Rozier, editors, NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, volume 11460 of Lecture Notes in Computer Science, pages 148-165. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-20652-9_10.
  15. Asta Halkjær From. Formalized soundness and completeness of epistemic logic. In Alexandra Silva, Renata Wassermann, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Virtual Event, October 5-8, 2021, Proceedings, volume 13038 of Lecture Notes in Computer Science, pages 1-15. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88853-4_1.
  16. Asta Halkjær From, Frederik Krogsdal Jacobsen, and Jørgen Villadsen. SeCaV: A sequent calculus verifier in Isabelle/HOL. In Mauricio Ayala-Rincon and Eduardo Bonelli, editors, Proceedings 16th Logical and Semantic Frameworks with Applications, Buenos Aires, Argentina (Online), 23rd - 24th July, 2021, volume 357 of Electronic Proceedings in Theoretical Computer Science, pages 38-55. Open Publishing Association, 2022. URL: https://doi.org/10.4204/EPTCS.357.4.
  17. Asta Halkjær From. Epistemic logic: Completeness of modal logics. Archive of Formal Proofs, October 2018. Formal proof development. URL: https://isa-afp.org/entries/Epistemic_Logic.html.
  18. Asta Halkjær From and Frederik Krogsdal Jacobsen. A sequent calculus prover for first-order logic with functions. Archive of Formal Proofs, January 2022. Formal proof development. URL: https://isa-afp.org/entries/FOL_Seq_Calc2.html.
  19. Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull, and Jørgen Villadsen. Teaching a formalized logical calculus. Electronic Proceedings in Theoretical Computer Science, 313:73-92, 2020. URL: https://doi.org/10.4204/EPTCS.313.5.
  20. Asta Halkjær From, Jørgen Villadsen, and Patrick Blackburn. Isabelle/HOL as a meta-language for teaching logic. Electronic Proceedings in Theoretical Computer Science, 328:18-34, October 2020. URL: https://doi.org/10.4204/eptcs.328.2.
  21. Frederik Krogsdal Jacobsen. Formalization of logical systems in Isabelle: An automated theorem prover for the Sequent Calculus Verifier. Master’s thesis, Technical University of Denmark, June 2021. URL: https://findit.dtu.dk/en/catalog/2691928304.
  22. Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull, and Jørgen Villadsen. Programming and verifying a declarative first-order prover in Isabelle/HOL. AI Communications, 31(3):281-299, 2018. URL: https://doi.org/10.3233/AIC-180764.
  23. Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. Locales - A sectioning concept for Isabelle. In Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, and Laurent Théry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, volume 1690 of Lecture Notes in Computer Science, pages 149-166. Springer, 1999. URL: https://doi.org/10.1007/3-540-48256-3_11.
  24. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. Lecture Notes in Computer Science, 8044, 2013. URL: https://doi.org/0.1007/978-3-642-39799-8_1.
  25. Ondrej Kunčar and Andrei Popescu. From types to sets by local type definition in higher-order logic. Journal of Automated Reasoning, 62(2):237-260, 2019. URL: https://doi.org/10.1007/s10817-018-9464-6.
  26. Peter Lammich. The GRAT tool chain. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, pages 457-463, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-66263-3_29.
  27. Peter Lammich. Efficient verified (UN)SAT certificate checking. Journal of Automated Reasoning, 64(3):513-532, 2020. URL: https://doi.org/10.1007/s10817-019-09525-z.
  28. Stephane Lescuyer. Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. Phd thesis, Université Paris Sud - Paris XI, January 2011. URL: https://tel.archives-ouvertes.fr/tel-00713668.
  29. Filip Marić. Formal verification of modern SAT solvers. Archive of Formal Proofs, July 2008. Formal proof development. URL: https://isa-afp.org/entries/SATSolverVerification.html.
  30. Filip Marić. Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theoretical Computer Science, 411(50):4333-4356, 2010. URL: https://doi.org/10.1016/j.tcs.2010.09.014.
  31. Filip Marić, Mirko Spasić, and René Thiemann. An incremental simplex algorithm with unsatisfiable core generation. Archive of Formal Proofs, August 2018. Formal proof development. URL: https://isa-afp.org/entries/Simplex.html.
  32. Julius Michaelis and Tobias Nipkow. Propositional proof systems. Archive of Formal Proofs, June 2017. Formal proof development. URL: https://isa-afp.org/entries/Propositional_Proof_Systems.html.
  33. Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, 23rd International Conference on Types for Proofs and Programs (TYPES 2017), volume 104 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.5.
  34. Dominique Pastre. MUSCADET 2.3: A knowledge-based theorem prover based on natural deduction. Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2083:685-689, 2001. URL: https://doi.org/10.1007/3-540-45744-5_56.
  35. Francis Jeffry Pelletier. Automated natural deduction in THINKER. Studia Logica, 60(1):3-43, 1998. URL: https://doi.org/10.1023/A:1005035316026.
  36. Nicolas Peltier. Propositional resolution and prime implicates generation. Archive of Formal Proofs, March 2016. Formal proof development. URL: https://isa-afp.org/entries/PropResPI.html.
  37. Nicolas Peltier. A variant of the superposition calculus. Archive of Formal Proofs, September 2016. Formal proof development. URL: https://isa-afp.org/entries/SuperCalc.html.
  38. Tom Ridge and James Margetson. A mechanically verified, sound and complete theorem prover for first order logic. Lecture Notes in Computer Science, 3603:294-309, 2005. URL: https://doi.org/10.1007/11541868_19.
  39. Anders Schlichtkrull. Formalization of the resolution calculus for first-order logic. Journal of Automated Reasoning, 61(1–4):455-484, 2018. URL: https://doi.org/10.1007/s10817-017-9447-z.
  40. Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. A verified prover based on ordered resolution. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 152-165, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294100.
  41. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann. Formalizing Bachmair and Ganzinger’s ordered resolution prover. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning, pages 89-107, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-94205-6_7.
  42. Anders Schlichtkrull and Jørgen Villadsen. Paraconsistency. Archive of Formal Proofs, December 2016. Formal proof development. URL: https://isa-afp.org/entries/Paraconsistency.html.
  43. Natarajan Shankar and Marc Vaucher. The mechanical verification of a DPLL-based satisfiability solver. Electronic Notes in Theoretical Computer Science, 269:3-17, 2011. Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop (LSFA 2010). URL: https://doi.org/10.1016/j.entcs.2011.03.002.
  44. Raymond M. Smullyan. First-order logic. Dover Publications, 1995. Google Scholar
  45. Mirko Spasić and Filip Marić. Formalization of incremental simplex algorithm by stepwise refinement. In Dimitra Giannakopoulou and Dominique Méry, editors, FM 2012: Formal Methods, pages 434-449, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-32759-9_35.
  46. Jørgen Villadsen, Asta Halkjær From, Alexander Birch Jensen, and Anders Schlichtkrull. Interactive theorem proving for logic and information. In Roussanka Loukanova, editor, Natural Language Processing in Artificial Intelligence - NLPinAI 2021, pages 25-48, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-90138-7_2.
  47. Jørgen Villadsen and Frederik Krogsdal Jacobsen. Using Isabelle in two courses on logic and automated reasoning. In João F. Ferreira, Alexandra Mendes, and Claudio Menghi, editors, Formal Methods Teaching, pages 117-132, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-91550-6_9.
  48. Jørgen Villadsen and Anders Schlichtkrull. Formalizing a paraconsistent logic in the Isabelle proof assistant. In Abdelkader Hameurlain, Josef Küng, Roland Wagner, and Hendrik Decker, editors, Transactions on Large-Scale Data- and Knowledge-Centered Systems XXXIV: Special Issue on Consistency and Inconsistency in Data-Centric Applications, pages 92-122, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-55947-5_5.
  49. Jørgen Villadsen, Andreas Halkjær From, and Anders Schlichtkrull. Natural deduction assistant (NaDeA). Electronic Proceedings in Theoretical Computer Science, 290(290):14-29, 2019. URL: https://doi.org/10.4204/EPTCS.290.2.
  50. Jørgen Villadsen, Anders Schlichtkrull, and Andreas Halkjær From. A verified simple prover for first-order logic. CEUR Workshop Proceedings, 2162:88-104, 2018. URL: http://ceur-ws.org/Vol-2162/#paper-08.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact