Logic and Modeling, Period 5, 2020

In Spring 2020 I taught Logic and Modeling, a second-year undergraduate course in theoretical computer science, at the VU. Due to COVID-19, the course was entirely online. Lectures were pre-recorded in 10 minute video clips. For each lecture, I hosted a live Q&A session via video meeting. Exercise classes were also held live by the course teaching assistants, Geoffrey Frankhuizen and Katrin Obendrauf.

For archival purposes, I have collected here the lectures and the recordings of live sessions.

Syllabus

The official (pre-COVID) syllabus is available here.

Briefly, Logic and Modeling is an introduction to different logical languages as tools for specification and verification. The course covers syntax, semantics, and derivations in propositional and first order logic; syntax and Kripke semantics of modal logic; metatheorems of the different logics, including soundness, completeness, and (un)decidability; and the structure of informal mathematical proofs.

The pen-and-paper presentations of propositional and first order logic are supplemented by the use of Lean, a tool that can check logical proofs automatically. Lean and similar systems are used “in the wild” for software verification, giving the course a practical component.

The first nine lectures, through propositional logic, follow the text Logic and Proof, which I have written with Jeremy Avigad and Floris van Doorn. The remaining lectures, on modal logic and metatheorems, follow Huth and Ryan’s Logic in Computer Science.

Archived Canvas pages

Course materials were distributed over Canvas. I have archived a few relevant pages here for public consumption.

• Lecture schedule
• Exercise class schedule
• Assignment information

Lectures

Unfortunately the Kaltura interface makes it somewhat inconvenient to publicize these videos. I have collected the videos for each lecture on one single page. Some mobile platforms do not display them with full features: you should be able to choose between seeing my screen, my face, or either embedded in the other.

• Lecture 1
• Lecture 2
• Lecture 3
• Lecture 4
• Lecture 5
• Lecture 6
• Lecture 7
• Lecture 8
• Lecture 9
• Lecture 10 – catchup day
• Lecture 11
• Lecture 12
• Lecture 13
• Lecture 14
• Extra videos about Lean as a software verification tool

Exercise Classes

My wonderful TAs recorded their live exercise sessions.

• Exercise Class 1 (Wednesday, April 1): Part 1, Part 2
• Exercise Class 2 (Friday, April 3)
• Exercise Class 3 (Wednesday, April 8): Part 1, Part 2
• Exercise Class 4 (Wednesday, April 15): Part 1, Part 2
• Exercise Class 5 (Friday, April 17)
• Exercise Class 6 (Wednesday, April 22): Part 1, Part 2
• Exercise Class 7 (Friday, April 24)
• Exercise Class 8 (Wednesday, April 29): Part 1, Part 2
• Exercise Class 9 (Friday, May 1)
• Exercise Class 10 (Wednesday, May 6): Part 1, Part 2
• Exercise Class 11 (Friday, May 8)
• Exercise Class 12 (Wednesday, May 13): Part 1, Part 2
• Exercise Class 13 (Friday, May 15)
• Exercise Class 14 (Wednesday, May 20)

Q&A Sessions

At each scheduled lecture time, I hosted a live Q&A session.