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 | |
|---|---|
| Coq | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Agda | Interactive system for writing and checking proofs |
| Lean | Programming language and theorem prover |
| Matita | Experimental, interactive theorem prover |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |