LISA

A Proof Assistant based on first order logic, sequent calculus and set theory.

LISA is a proof assistant built on first-order logic and sequent calculus, with a foundational layer in axiomatic set theory. It provides a kernel that checks proof certificates for validity and a higher-level tactic language in Scala for constructing and automating proofs interactively.