Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
This lecture introduces the LISA proof assistant, focusing on its codebase organization, the kernel package containing trusted code for theorem production and proof verification, the FOL package for First Order Logic formalization, and the proof package built on top of FOL for defining sequents, proof steps, and theorems.