Document Open Access Logo

LISA - A Modern Proof System

Authors Simon Guilloud , Sankalp Gambhir , Viktor Kunčak

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.17.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Author Details

Simon Guilloud
  • Laboratory for Automated Reasoning and Analysis, EPFL, Lausanne, Switzerland
Sankalp Gambhir
  • Laboratory for Automated Reasoning and Analysis, EPFL, Lausanne, Switzerland
Viktor Kunčak
  • Laboratory for Automated Reasoning and Analysis, EPFL, Lausanne, Switzerland

Cite AsGet BibTex

Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak. LISA - A Modern Proof System. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.17

Abstract

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and function symbols. It implements polynomial-time proof checking and uses the axioms of ortholattices (which implies the irrelevance of the order of conjuncts and disjuncts and additional propositional laws). The kernel supports the notion of theorems (whose proofs are not expanded), as well as definitions of predicate symbols and objects whose unique existence is proven. A domain-specific language enables construction of proofs and development of proof tactics with user-friendly tools and presentation, while remaining within the general-purpose language, Scala. We describe the LISA proof system and illustrate the flavour and the level of abstraction of proofs written in LISA. This includes a proof-generating tactic for propositional tautologies, leveraging the ortholattice properties to reduce the size of proofs. We also present early formalization of set theory in LISA, including Cantor’s theorem.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Proof assistant
  • First Order Logic
  • Set Theory

Metrics

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

Supplementary Materials

References

  1. Rob Arthan. HOL Constant Definition Done Right. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, Lecture Notes in Computer Science, pages 531-536, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-08970-6_34.
  2. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 13243, pages 415-442. Springer International Publishing, Cham, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  3. Ladislav Beran. Orthomodular Lattices (An Algebraic Approach). Springer Dordrecht, 1985. URL: https://doi.org/10.1007/978-94-009-5215-7.
  4. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer-Verlag, Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-662-07964-5.
  5. Chad E. Brown. Satallax: An automatic higher-order prover. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning, pages 111-117, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  6. Chad E. Brown, C. Kaliszyk, and Karol Pak. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. In ITP, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.9.
  7. Gunter Bruns and John Harding. Algebraic aspects of orthomodular lattices. In Bob Coecke, David Moore, and Alexander Wilce, editors, Current Research in Operational Quantum Logic: Algebras, Categories, Languages, pages 37-65. Springer Netherlands, Dordrecht, 2000. URL: https://doi.org/10.1007/978-94-017-1201-9_2.
  8. Paul J. Cohen. The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the United States of America, 50(6):1143-1148, 1963. URL: http://www.jstor.org/stable/71858.
  9. Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, FM 2012: Formal Methods, pages 147-154, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  10. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, July 1962. URL: https://doi.org/10.1145/368273.368557.
  11. Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. Elsevier, 1972. Google Scholar
  12. 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, volume 9195, pages 378-388. Springer International Publishing, Cham, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  13. David Delahaye. A tactic language for the system coq. In LPAR, volume 1955, pages 85-95. Springer, 2000. Google Scholar
  14. Harald Ganzinger, Christoph Meyer, and Christoph Weidenbach. Soft typing for ordered resolution. In William McCune, editor, Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, volume 1249 of Lecture Notes in Computer Science, pages 321-335. Springer, 1997. URL: https://doi.org/10.1007/3-540-63104-6_32.
  15. G. Gentzen. Untersuchungen über das logische schließen i. Mathematische Zeitschrift, 39:176-210, 1935. URL: http://eudml.org/doc/168546.
  16. Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth, and P. Ted Christopher. Edinburgh LCF: a mechanized logic of computation. Lecture Notes in Computer Science, 1978. Google Scholar
  17. Simon Guilloud. LISA Reference Manual. EPFL-LARA, February 2023. Google Scholar
  18. Simon Guilloud, Mario Bucev, Dragana Milovancevic, and Viktor Kunčak. Formula normalizations in verification. Technical Report 297701, EPFL, 2023. URL: http://infoscience.epfl.ch/record/297701.
  19. Simon Guilloud and Viktor Kunčak, editors. Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. Springer, 2022. URL: https://doi.org/10.48550/arXiv.2110.03315.
  20. Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, and Matías Steinberg. The independence of the continuum hypothesis in isabelle/zf. Archive of Formal Proofs, March 2022. , Formal proof development. URL: https://isa-afp.org/entries/Independence_CH.html.
  21. J Harding. Quantum monadic algebras. Journal of Physics A: Mathematical and Theoretical, 55(39):394001, September 2022. URL: https://doi.org/10.1088/1751-8121/ac845b.
  22. John Harrison. HOL Light: An Overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, volume 5674, pages 60-66. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_4.
  23. John Harrison. Let’s make set theory great again! In Axiomatic Set Theory, page 46, Aussois, 2018. Google Scholar
  24. CNRS Inria and contributors. Ltac2 — Coq 8.16.1 documentation. URL: https://coq.inria.fr/refman/proof-engine/ltac2.html.
  25. Himanshu Jain, Constantinos Bartzis, and Edmund Clarke. Satisfiability checking of non-clausal formulas using general matings. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, pages 75-89, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11814948_10.
  26. Thomas Jech. Set theory: The third millennium edition, revised and expanded. Springer, 2003. Google Scholar
  27. Deepak Kapur and Paliath Narendran. Complexity of unification problems with associative-commutative operators. J. Autom. Reason., 9(2):261-288, 1992. URL: https://doi.org/10.1007/BF00245463.
  28. Laura Kovács and Andrei Voronkov. First-Order Theorem Proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, Lecture Notes in Computer Science, pages 1-35, Berlin, Heidelberg, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-39799-8_1.
  29. Norman Megill. Metamath. The Seventeen Provers of the World: Foreword by Dana S. Scott, pages 88-95, 2006. Google Scholar
  30. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing. Google Scholar
  31. Adam Naumowicz and Artur Kornilowicz. A Brief Overview of Mizar. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674, pages 67-72, August 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_5.
  32. Martin Odersky, Aggelos Biboudis, Fengyun Liu, and Olivier Blanvillain. Foundations of implicit function types. Technical report, EPFL, 2017. URL: http://infoscience.epfl.ch/record/229203.
  33. Lawrence C. Paulson. Isabelle: The next 700 theorem provers. CoRR, cs.LO/9301106, 1993. URL: https://arxiv.org/abs/cs/9301106.
  34. Lawrence C. Paulson. A generic tableau prover and its integration with Isabelle. JUCS - Journal of Universal Computer Science, 5(3):73-87, 1999. URL: https://doi.org/10.3217/jucs-005-03-0073.
  35. Lawrence C Paulson. Isabelle’s logics: FOL and ZF, 2013. Google Scholar
  36. Lawrence C. Paulson. Zermelo Fraenkel set theory in higher-order logic. Archive of Formal Proofs, October 2019. , Formal proof development. URL: https://isa-afp.org/entries/ZFC_in_HOL.html.
  37. TLA Proof System Project. TLA+ proof system. URL: https://tla.msr-inria.inria.fr/tlaps/content/Home.html.
  38. Stephan Schulz. System Description: E 1.8. In Ken McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, pages 735-743, Berlin, Heidelberg, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-45221-5_49.
  39. Alexander Steen. Leo-iii 1.7, July 2022. URL: https://doi.org/10.5281/zenodo.7650205.
  40. Christian Urban. The Isabelle Cookbook. URL: https://web.cs.wpi.edu/~dd/resources_isabelle/isabelle_programming.urban.pdf.
  41. Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making Higher-Order Superposition Work. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction endash CADE 28, Lecture Notes in Computer Science, pages 415-432, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-79876-5_24.
  42. Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. SPASS Version 3.5. In Renate A. Schmidt, editor, Automated Deduction endash CADE-22, Lecture Notes in Computer Science, pages 140-145, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-02959-2_10.
  43. Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle Framework. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, pages 33-38, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-71067-7_7.
  44. Benjamin Werner. Sets in types, types in sets. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Martín Abadi, and Takayasu Ito, editors, Theoretical Aspects of Computer Software, volume 1281, pages 530-546. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. URL: https://doi.org/10.1007/BFb0014566.
  45. Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.
  46. Bohua Zhan. Formalization of the Fundamental Group in Untyped Set Theory Using Auto2. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, Lecture Notes in Computer Science, pages 514-530, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-66107-0_32.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact