License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.17
URN: urn:nbn:de:0030-drops-183922
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18392/
Guilloud, Simon ;
Gambhir, Sankalp ;
Kunčak, Viktor
LISA - A Modern Proof System
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.
BibTeX - Entry
@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/opus/volltexte/2023/18392},
URN = {urn:nbn:de:0030-drops-183922},
doi = {10.4230/LIPIcs.ITP.2023.17},
annote = {Keywords: Proof assistant, First Order Logic, Set Theory}
}
