Search Results

Documents authored by Guilloud, Simon

Artifact
Software
DOI: 10.4230/artifacts.22517
epfl-lara/lisa

Authors: Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak

Abstract
Cite as

Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kunčak. epfl-lara/lisa (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22517,
   title = {{epfl-lara/lisa}}, 
   author = {Guilloud, Simon and Gambhir, Sankalp and Gilot, Andrea and Kun\v{c}ak, Viktor},
   note = {Software, version 0.1., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:c3f6e63aa274ed7ea292efcb0eade3f4abb60d2a;origin=https://github.com/epfl-lara/lisa;visit=swh:1:snp:64f8fc9f8972d4d54804632b32b91b51eee621fb;anchor=swh:1:rev:9976621a9198b3a81aeb1e49a952bc0e232ea491}{\texttt{swh:1:dir:c3f6e63aa274ed7ea292efcb0eade3f4abb60d2a}} (visited on 2024-11-28)},
   url = {https://github.com/epfl-lara/lisa/tree/itp2024-archive},
   doi = {10.4230/artifacts.22517},
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.18
Mechanized HOL Reasoning in Set Theory

Authors: Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assume traditional FOL syntax without notation for term-level binders. To embed λ-terms, we define a notion of context, defining the closure of all abstractions occuring inside a term. We implement the embedding in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory (presented at ITP 2023). We show how to implement type checking and the proof steps of HOL Light as proof-producing tactics in Lisa. The embedded HOL theorems and proofs are interoperable with the existing Lisa library. This yields a form of soft type system supporting top-level polymorphism and ADTs within set theory. The approach offers tools for Lisa users to carry HOL-style proofs within set theory. It also enables the import of HOL Light theorem statements into Lisa, as well as the replay of small HOL Light kernel proofs.
Cite as

Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kunčak. Mechanized HOL Reasoning in Set Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guilloud_et_al:LIPIcs.ITP.2024.18,
  author =	{Guilloud, Simon and Gambhir, Sankalp and Gilot, Andrea and Kun\v{c}ak, Viktor},
  title =	{{Mechanized HOL Reasoning in Set Theory}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.18},
  URN =		{urn:nbn:de:0030-drops-207464},
  doi =		{10.4230/LIPIcs.ITP.2024.18},
  annote =	{Keywords: Proof assistant, First Order Logic, Set Theory, Higher Order Logic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.17
LISA - A Modern Proof System

Authors: Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{guilloud_et_al:LIPIcs.ITP.2023.17,
  author =	{Guilloud, Simon and Gambhir, Sankalp and Kun\v{c}ak, Viktor},
  title =	{{LISA - A Modern Proof System}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{17:1--17:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.17},
  URN =		{urn:nbn:de:0030-drops-183922},
  doi =		{10.4230/LIPIcs.ITP.2023.17},
  annote =	{Keywords: Proof assistant, First Order Logic, Set Theory}
}
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 About DROPS Imprint Privacy Contact