Document Open Access Logo

A Modular Formalization of Superposition in Isabelle/HOL

Authors Martin Desharnais , Balazs Toth , Uwe Waldmann , Jasmin Blanchette , Sophie Tourret

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.12.pdf
  • Filesize: 0.79 MB
  • 20 pages

Document Identifiers

Author Details

Martin Desharnais
  • Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany
  • Graduate School of Computer Science, Saarland Informatics Campus, Saarbrücken, Germany
Balazs Toth
  • Ludwig-Maximilians-Universität München, Germany
Uwe Waldmann
  • Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany
Jasmin Blanchette
  • Ludwig-Maximilians-Universität München, Germany
  • Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany
Sophie Tourret
  • Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
  • Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • Blanchette, Jasmin: Co-funded by the European Union (ERC, Nekoka, 101083038). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

Acknowledgements

We thank Xavier Généreux, Mark Summerfield, and the anonymous reviewers for suggesting textual improvements.

Cite AsGet BibTex

Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A Modular Formalization of Superposition in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.12

Abstract

Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers. It works by saturating the given set of clauses and is refutationally complete, meaning that if the set is inconsistent, the saturation will contain a contradiction. In this work, we restructured the completeness proof to cleanly separate the ground (i.e., variable-free) and nonground aspects, and we formalized the result in Isabelle/HOL. We relied on the IsaFoR library for first-order terms and on the Isabelle saturation framework.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Theorem proving algorithms
Keywords
  • Superposition
  • verification
  • first-order logic
  • higher-order logic

Metrics

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

Supplementary Materials

References

  1. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  2. Leo Bachmair and Harald Ganzinger. On restrictions of ordered paramodulation with simplification. In Mark E. Stickel, editor, CADE-10, volume 449 of LNCS, pages 427-441. Springer, 1990. URL: https://doi.org/10.1007/3-540-52885-7_105.
  3. Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput., 4(3):217-247, 1994. Google Scholar
  4. Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 19-99. Elsevier and MIT Press, 2001. Google Scholar
  5. Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Theorem proving for hierarchic first-order theories. In Hélène Kirchner and Giorgio Levi, editors, ALP '92, volume 632 of LNCS, pages 420-434. Springer, 1992. Google Scholar
  6. Peter Baumgartner and Uwe Waldmann. Hierarchic superposition revisited. In Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, and Frank Wolter, editors, Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, volume 11560 of LNCS, pages 15-56. Springer, 2019. Google Scholar
  7. Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann. Superposition for lambda-free higher-order logic. Log. Methods Comput. Sci., 17(2), 2021. Google Scholar
  8. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirovic. Superposition for higher-order logic. J. Autom. Reason., 67(1):10, 2023. Google Scholar
  9. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovic, and Uwe Waldmann. Superposition with lambdas. J. Autom. Reason., 65(7):893-940, 2021. Google Scholar
  10. Ahmed Bhayat and Giles Reger. A combinator-based superposition calculus for higher-order logic. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR 2020, Part I, volume 12166 of LNCS, pages 278-296. Springer, 2020. Google Scholar
  11. Ahmed Bhayat, Johannes Schoisswohl, and Michael Rawson. Superposition with delayed unification. In Brigitte Pientka and Cesare Tinelli, editors, CADE-29, volume 14132 of LNCS, pages 23-40. Springer, 2023. Google Scholar
  12. 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, CPP 2019, pages 1-13. ACM, 2019. Google Scholar
  13. Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart, and incrementality. J. Autom. Reason., 61(3):333-366, 2018. Google Scholar
  14. Jasmin Christian Blanchette and Sophie Tourret. Extensions to the comprehensive framework for saturation theorem proving. Archive of Formal Proofs, 2020. URL: https://isa-afp.org/entries/Saturation_Framework_Extensions.html.
  15. Martin Bromberger, Martin Desharnais, and Christoph Weidenbach. An Isabelle/HOL formalization of the SCL(FOL) calculus. In Brigitte Pientka and Cesare Tinelli, editors, CADE-29, volume 14132 of LNCS, pages 116-133. Springer, 2023. Google Scholar
  16. Simon Cruanes. Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. Ph.D. thesis, École polytechnique, 2015. Google Scholar
  17. Martin Desharnais and Balazs Toth. Superposition calculus, 2024. URL: https://github.com/IsaFoL/IsaFoL/tree/ITP2024-IsaSuperposition/Superposition_Calculus.
  18. Alberto Fiori and Christoph Weidenbach. SCL clause learning from simple models. In Pascal Fontaine, editor, CADE-27, volume 11716 of LNCS, pages 233-249. Springer, 2019. Google Scholar
  19. Asta Halkjær From, Patrick Blackburn, and Jørgen Villadsen. Formalizing a Seligman-style tableau system for hybrid logic (short paper). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, IJCAR 2020, Part I, volume 12166 of LNCS, pages 474-481. Springer, 2020. Google Scholar
  20. Asta Halkjær From, Anders Schlichtkrull, and Jørgen Villadsen. A sequent calculus for first-order logic formalized in Isabelle/HOL. J. Log. Comput., 33(4):818-836, 2023. Google Scholar
  21. John Harrison. Formalizing basic first order model theory. In Jim Grundy and Malcolm C. Newey, editors, TPHOLs '98, volume 1479 of LNCS, pages 153-170. Springer, 1998. Google Scholar
  22. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, CAV 2013, volume 8044 of LNCS, pages 1-35. Springer, 2013. Google Scholar
  23. Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, and Thomas Sternagel. Regular tree relations. Archive of Formal Proofs, 2021. URL: https://isa-afp.org/entries/Regular_Tree_Relations.html.
  24. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  25. Lawrence C. Paulson. A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. Rev. Symb. Log., 7(3):484-498, 2014. Google Scholar
  26. Lawrence C. Paulson. A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. J. Autom. Reason., 55(1):1-37, 2015. URL: https://doi.org/10.1007/S10817-015-9322-8.
  27. Nicolas Peltier. A variant of the superposition calculus. Archive of Formal Proofs, 2016. URL: https://www.isa-afp.org/entries/SuperCalc.html.
  28. Henrik Persson. Constructive completeness of intuitionistic predicate logic: A formalisation in type theory. Licentiate thesis, Chalmers tekniska högskola and Göteborgs universitet, 1996. Google Scholar
  29. John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965. Google Scholar
  30. 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. Google Scholar
  31. Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel. A verified prover based on ordered resolution. In Assia Mahboubi and Magnus O. Myreen, editors, CPP 2019, pages 152-165. ACM, 2019. Google Scholar
  32. Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, and Uwe Waldmann. Formalization of Bachmair and Ganzinger’s ordered resolution prover. Archive of Formal Proofs, 2018. URL: https://isa-afp.org/entries/Ordered_Resolution_Prover.html.
  33. Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. In Pascal Fontaine, editor, CADE-27, volume 11716 of LNCS, pages 495-507. Springer, 2019. Google Scholar
  34. Natarajan Shankar. Metamathematics, Machines, and Gödel’s Proof, volume 38 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1994. Google Scholar
  35. Christian Sternagel and René Thiemann. Abstract rewriting. Archive of Formal Proofs, 2010. URL: https://isa-afp.org/entries/Abstract-Rewriting.html.
  36. Christian Sternagel and René Thiemann. First-order terms. Archive of Formal Proofs, 2018. URL: https://isa-afp.org/entries/First_Order_Terms.html.
  37. Christian Sternagel and René Thiemann. A formalization of Knuth–Bendix orders. Archive of Formal Proofs, 2020. URL: https://isa-afp.org/entries/Knuth_Bendix_Order.html.
  38. Lukas Stevens and Tobias Nipkow. A verified decision procedure for orders in Isabelle/HOL. In Zhe Hou and Vijay Ganesh, editors, ATVA 2021, volume 12971 of LNCS, pages 127-143. Springer, 2021. Google Scholar
  39. René Thiemann and Christian Sternagel. Certification of termination proofs using CeTA. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, TPHOLs 2009, volume 5674 of LNCS, pages 452-468. Springer, 2009. Google Scholar
  40. Sophie Tourret. A comprehensive framework for saturation theorem proving. Archive of Formal Proofs, 2020. URL: https://www.isa-afp.org/entries/Saturation_Framework.html.
  41. Sophie Tourret. The spawns of the saturation framework. In Laura Kovács and Michael Rawson, editors, 7th and 8th Vampire Workshop, volume 99 of EPiC Series in Computing, pages 1-6. EasyChair, 2024. Google Scholar
  42. Sophie Tourret and Jasmin Blanchette. A modular Isabelle framework for verifying saturation provers. In Cătălin Hrițcu and Andrei Popescu, editors, CPP 2021, pages 224-237. ACM, 2021. Google Scholar
  43. Uwe Waldmann. A modular completeness proof for the superposition calculus, 2024. URL: https://nekoka-project.github.io/pubs/isasup_blueprint.pdf.
  44. Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. A comprehensive framework for saturation theorem proving. J. Autom. Reason., 66(4):499-539, 2022. Google Scholar
  45. Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. SPASS version 3.5. In Renate A. Schmidt, editor, CADE-22, volume 5663 of LNCS, pages 140-145. Springer, 2009. 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