This project formalizes the basics of first-order logic and proves soundness of the common resolution rules in propositional and first-order logic. We achieve this by closely following Chapter 3 of the lecture notes from the course Automated Theorem Proving.
This project is licensed under the GPL v3 – see the LICENSE file for details.
Created by Norman Lohrer and Samuel Leßmann during the course 'Formalization in Lean' taught by Xavier Généreux at LMU in 2024/25.