Logic and Modeling 2020 -- Assignments

Lean is a proof assistant which, like natural deduction systems, are based on strictly formal rules for syntactic reasoning. Proof assistants are used to proof correctness of programs, protocols or mathematical theorems. You will learn that proof assistants are very strict! We hope that the use of proof assistants will be a valuable experience. If you develop safety-critical or life-critical systems, you should consider to use proof assistants to formally prove that your programs are correct.

To pass the practicum, you will need to solve a number of problems in Lean. We will use the web editor CoCalc to distribute and submit assignments.  You will receive an email inviting you to a CoCalc class. In this class you will find assignments, one for propositional logic and one for predicate logic and relations. To complete each assigned problem, replace the sorry with a proof that Lean accepts. Do not change the “variables A B C” line, the name of the theorem, or the formula you are trying to prove! You can submit the assignments through CoCalc.

The deadline for the first assignment is May 1. The deadline for the second assignment is May 15. (Note: because of COVID-19 interruptions, these are soft deadlines. All assignments completed before the end of the day on May 20 will be accepted.) You are expected to solve the tasks individually.