LISA (LISA Is Sets Automated) is a proof assistant based on first-order logic sequent calculus and set theory.
It provides a trusted kernel for checking proofs, together with a domain-specific language and supporting utilities for developing formal proofs, tactics, and mathematical theories.
This is free and open source software.
Key Features
- Based on first-order logic, sequent calculus, and set theory.
- Trusted kernel verifies all accepted theorems and proofs.
- Formalisation of first-order logic.
- Proofs formalised through sequent calculus.
- Domain-specific language for writing proofs and mathematical developments.
- Supports development of proof tactics.
- Parser and printer for proofs and formulas.
- Provides unification algorithms.
- Includes a mathematical library with set theory developments.
Website: github.com/epfl-lara/lisa
Support:
Developer: Laboratory for Automated Reasoning and Analysis (LARA)
License: Apache License 2.0
LISA is written in Scala. Learn Scala with our recommended free books and free tutorials.
Related Software
| Proof Assistants | |
|---|---|
| Rocq Prover | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Lean | Programming language and theorem prover |
| Agda | Interactive system for writing and checking proofs |
| F* | Functional language for verified programs with dependent refinement types |
| HOL4 | Interactive higher-order logic environment for rigorous theorem development |
| Aya | Dependently typed language for formalisation and certified programming |
| Lambdapi | Logical framework for defining and checking expressive type systems |
| HOL Light | Lightweight higher-order logic system with a small trusted kernel |
| PVS | Specification and verification suite for analysing complex systems |
| LISA | Scala-based platform for formal mathematics and automated reasoning |
Read our verdict in the software roundup.
 Explore our carefully curated directory of recommended free and open source software, covering every major software category.The directory forms part of our extensive collection of articles for Linux enthusiasts. It includes hundreds of detailed reviews, together with free and open source alternatives to proprietary software from companies such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. LinuxLinks also covers interesting projects worth exploring, Linux-compatible hardware, free programming books and tutorials, and much more. Know a useful free and open source Linux application that we haven’t covered? Tell us about it using our submission form. |
Please read our Comment Policy before commenting.