LISA is a Proof Assistant based on first order logic, sequent calculus and set theory. To get started, look at the Reference Manual.

EPFL-LARA Website: https://lara.epfl.ch/w/

The kernel package contains the trusted code of LISA, in the sense that it only can produce theorem and verify proof. Any bug or error in code written outside this package should not possibly break soundness. The kernel contains essentially two elements: Formalisation of First Order Logic, and Formalisation of Proofs through Sequent Calculus.

The proven package contains tactics and proofs

The TPTP package contains a parser from the TPTP file format to LISA. The simplest way to use it is to download the TPTP library and put it inside main/resources.

• sbt test to compile and execute the test suite
• sbt assembly to package it as a library
• sbt doc to generate the Scala documentation

Copyright 2022 EPFL

Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at

   http:https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.