Lecture slides and lecture notes are regularly posted as the semester progresses, typically early in the week in which they are presented.
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:
The main textbook for this course is Logic in Computer Science: Modelling and Reasoning About Systems, Second Edition, by Michael Huth and Mark Ryan. All references to this book in lecture notes and handouts are indicated by the acronym [LCS]. The course will cover three of the six chapters, about half of the book:
[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 logic-based tools. (Other parts of BDD's, not covered in [LCS], play important roles elsewhere, e.g., in the design and analysis of combinatorial algorithms.)
There are many Isabelle publications on the Web, some excellent but often addressed to a more advanced audience, already familiar with automated formal tools. However, for our purposes in Fall 2021, you will not need to go beyond the following monograph, which will be our main Isabelle reference:
Programming and Proving in Isabelle/HOL, by Tobias Nipkow.
The following are among the best tutorials on Z3, written by its two main developers, which contain many easy examples from across computer science. As with any tutorial, these are long documents. You should be picky and selective, i.e., just find the part or example that suits your purposes and copy it:
Z3 - A Tutorial, by Leonardo de Moura and Nikolaj Bjorner. Most of the examples are in Sections 5 to 12 (these are short sections, covering less than 20 pages all together).
Z3 - Guide, by Leonardo de Moura and Nikolaj Bjorner. This is an on-line interactive tutorial, sharing many of the examples of the preceding without being identical. It is friendly and easy to use.
Programming Z3, by Nikolaj Bjorner, Leonardo de Moura, Lev Nachmanson, and Christoph Wintersteiger. This is an on-line (not interactive) tutorial, somewhat more advanced than the preceding two. It presents many examples using the Python front-end Z3Py, the one which we propose to use this semester.
Z3 API in Python, by Leonardo de Moura. This is somewhat older than the preceding tutorials, containing an abundance of short examples from across computer science, many already in the preceding ones.