Document Open Access Logo

Formalizing Splitting in Isabelle/HOL

Authors Ghilain Bergeron , Florent Krasnopol , Sophie Tourret

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.22.pdf
  • Filesize: 0.81 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.22.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Theorem proving algorithms
Keywords
  • Isabelle/HOL
  • saturation-based calculi
  • splitting

Metrics

Abstract

We describe the formalization in Isabelle/HOL of a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. We focus here on the simplest splitting model and provide an extension of the ordered resolution calculus with a variant of splitting called Lightweight AVATAR.

Cite As Get BibTex

Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret. Formalizing Splitting in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.22

Author Details

Ghilain Bergeron
  • Inria, Loria, CNRS, Lorraine Univ., Nancy, France
Florent Krasnopol
  • ENS Paris-Saclay, France
Sophie Tourret
  • Inria, Loria, CNRS, Lorraine Univ., Nancy, France
  • Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • Tourret, Sophie: supported by the ANR project BLaSST (ANR-21-CE25-0010).

Acknowledgements

Asta Halkjær From contributed the theory Lazy_List_Limsup to the framework. Jasmin Blanchette and the anonymous reviewers suggested many improvements to the text. We thank them all.

References

  1. Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 19-99. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/b978-044450813-3/50004-7.
  2. Clemens Ballarin. Locales: A module system for mathematical theories. J. Autom. Reason., 52(2):123-153, 2014. URL: https://doi.org/10.1007/s10817-013-9284-7.
  3. Ghilain Bergeron, Florent Krasnopol, and Sophie Tourret. A modular splitting framework for saturation theorem proving. Archive of Formal Proofs, June 2025. , Formal proof development. URL: https://isa-afp.org/entries/Splitting_Framework.html.
  4. Jasmin Christian Blanchette and Sophie Tourret. Extensions to the comprehensive framework for saturation theorem proving. Archive of Formal Proofs, August 2020. , Formal proof development. URL: https://isa-afp.org/entries/Saturation_Framework_Extensions.html.
  5. Martin Desharnais and Balazs Toth. A modular formalization of superposition. Archive of Formal Proofs, October 2024. , Formal proof development. URL: https://isa-afp.org/entries/Superposition_Calculus.html.
  6. Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A modular formalization of superposition in Isabelle/HOL. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia, volume 309 of LIPIcs, pages 12:1-12:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.12.
  7. Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret. Unifying splitting. J. Autom. Reason., 67(2):16, 2023. URL: https://doi.org/10.1007/s10817-023-09660-8.
  8. Arnaud Fietzke and Christoph Weidenbach. Labelled splitting. Ann. Math. Artif. Intell., 55(1-2):3-34, 2009. URL: https://doi.org/10.1007/s10472-009-9150-9.
  9. John Harrison. Formalizing basic first order model theory. In TPHOLs, volume 1479 of Lecture Notes in Computer Science, pages 153-170. Springer, 1998. URL: https://doi.org/10.1007/BFB0055135.
  10. 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, May 29-June 1, 2017, Budapest, Hungary, volume 104 of LIPIcs, pages 5:1-5:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.5.
  11. 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.
  12. Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 371-443. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/b978-044450813-3/50009-6.
  13. Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Revisiting enumerative instantiation. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, volume 10806 of Lecture Notes in Computer Science, pages 112-131. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89963-3_7.
  14. Alexandre Riazanov and Andrei Voronkov. Splitting without backtracking. In Bernhard Nebel, editor, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI 2001, Seattle, Washington, USA, August 4-10, 2001, pages 611-617. Morgan Kaufmann, 2001. Google Scholar
  15. Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, and Uwe Waldmann. Formalizing Bachmair and Ganzinger’s ordered resolution prover. J. Autom. Reason., 64(7):1169-1195, 2020. URL: https://doi.org/10.1007/s10817-020-09561-0.
  16. Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. A verified functional implementation of Bachmair and Ganzinger’s ordered resolution prover. Arch. Formal Proofs, 2018, 2018. URL: https://www.isa-afp.org/entries/Functional_Ordered_Resolution_Prover.html.
  17. Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. A verified prover based on ordered resolution. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 152-165. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294100.
  18. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann. Formalization of Bachmair and Ganzinger’s ordered resolution prover. Archive of Formal Proofs, January 2018. , Formal proof development. URL: https://isa-afp.org/entries/Ordered_Resolution_Prover.html.
  19. Sophie Tourret and Jasmin Blanchette. A modular Isabelle framework for verifying saturation provers. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 224-237. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439912.
  20. Andrei Voronkov. AVATAR: the architecture for first-order theorem provers. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 696-710. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_46.
  21. Petar Vukmirovic, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. J. Autom. Reason., 66(4):541-564, 2022. URL: https://doi.org/10.1007/s10817-021-09613-z.
  22. Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. A comprehensive framework for saturation theorem proving. J. Autom. Reason., 66(4):499-539, 2022. URL: https://doi.org/10.1007/s10817-022-09621-7.
  23. Max Zorn. A remark on method in transfinite algebra. Bulletin of the American Mathematical Society, 41(10):667-670, 1935. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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