This webpage is a guide to further reading material, if you wish to go deeper into topics presented during the semester. It is an evolving guide, with constant additions to complement material presented in lecture. You will not be responsible for studying the documents posted on this webpage.
Systems of Formal Proofs:
The following handouts are lecture notes I wrote for a course I taught twice at other universities, and once in the Mathematics Department at BU many years ago.
Tools for Automated and Semi-Automated Formal Reasoning (click here).
Compactness and Completeness Theorems of Propositional and First-Order Logic (click here).
Formal Modeling with Boolean Formulas (click here).
Formal Modeling with Quantified Boolean Formulas (QBF's) (click here).
Donald Knuth on Binary Decision Diagrams (BDD's) (click here).
Exercises in First-Order Definability (click here).
Undecidability of First-Order Validity (click here -- does not preview well in Chrome and perhaps other browsers too).