Lecture slides and lecture notes are regularly posted at the Piazza website for CS 511 (only accessible to students registered for the course) and as the semester progresses, typically early in the week in which they are presented. On this webpage, only headings of topics covered every week will be listed.
Week 1:
Week 2:
Week 3:
Week 4:
Week 5:
Week 6:
Week 7:
Week 8:
Week 9:
Week 10:
Week 11:
Week 12:
Week 13:
Week 14:
In addition to lecture notes downloadable from the Piazza website for CS 511, we will use two books as external references:
The book Logic in Computer Science: Modelling and Reasoning About Systems, Second Edition, by Michael Huth and Mark Ryan. References to this book in lecture notes and handouts will be indicated by the acronym [LCS].
The book The Mechanics of Proof by Heather Macbeth. References to this book in lecture notes and handouts will be indicated by the acronym [MoP].
The course covers three of the six chapters in the first book [LCS], about half of it, and about an equal amount of additional material presented in lecture notes :
[LCS, Chapter 1] presents basic notions and results of classical Propositional Logic, including the essential background for SAT solvers.
[LCS, Chapter 2] presents basic results of classical Predicate Logic (aka First-Order Logic), which includes the essential background for SMT solvers in addition to basic results in relation to limits of expressibility and complexity of logical formalisms.
[LCS, Chapter 6] is on Binary Decision Diagrams (aka BDD's). This chapter is an introduction to a wide-ranging topic, only a small part of which has a bearing on the efficient implementation of SAT/SMT solvers and other automated formal tools. (Other parts of BDD's, not covered in [LCS], play important roles elsewhere, e.g., in the design and analysis of combinatorial algorithms.)
Students are expected to use the second book [MoP] as a manual for how to write solutions of homework exercises, only the exercises that are explicitly required to be done with the Lean proof assistant. Much of the reading of [MoP] will be left to the students to do on their own and inasmuch as they need to do their homework; the presentation in [MoP] is easy, friendly, and gradually building up to the level you will need for the homework assignments.
Warning: There is a profusion of material on the Lean proof assistant, available for free download from the Web. It is enormous and you will be overwhelmed if you try to consult it, especially if you are new to this area of computer science. You are therefore highly encouraged to limit your reading and study of Lean to the book [MoP], which covers all that you will need for homework.