Homework Assignments

• HW #01: handout, propositional logic
• HW #02: handout, games and puzzles with Z3 and Z3Py
• HW #03: handout, propositional logic and quantified Boolean formulas
• HW #04: handout, graph problems with Z3Py
• HW #05: handout, problems of first-order definability
• HW #06: handout, pseudo-Boolean optimization and applications with Z3Py
• HW #07: handout, problems of compactness and completeness in first-order logic
• HW #08: handout, probabilistic graphical models (Bayesian networks) with Z3Py
• HW #09: handout, tableaux method for FOL, limits of first-order definability
• HW #10: handout, program analysis via program unwinding
• HW #11: handout, abstract interpretation, second-order definability
• HW #12: handout, program synthesis

Exams

• Mid-term exam, October 24, 2019: handout, selected solutions posted on Piazza webpage
• End-of-term exam, December 16, 2019: handout, selected solutions posted on Piazza webpage

Additional Resources

Typesetting with LaTeX: If you do not have prior experience with LaTeX, you will need to learn as much of it as you need to format your technical documents (homework assignments, lecture notes, and more). The best way to learn what you need is to copy (yes, copy!) LaTeX sources produced by others. Below are useful documents produced with LaTeX, both the pdf files and the source files:

• Scribe template, for note-takers during lecture (tex source, pdf file).
• Another scribe template, for note-takers during lecture (tex source, pdf file) -- courtesy of Sarah Bargal.
• Examples of natural deductions (tex source, pdf file). To compile this tex file, you will need the following packages, if they are not already available in your computer: prooftree.sty and boxproof.sty. Place these two packages in the same directory where the tex file is located.
• Other examples of natural deductions (tex source, pdf file). To compile this tex file, place the following packages in the same directory where the tex file is located: flagderiv.sty, logicproof.sty, and bussproofs.sty.
• Warning: Some of the commands in the packages {prooftree.sty, boxproof.sty} conflict with some of the commands in the packages {flagderiv.sty, logicproof.sty, bussproofs.sty}. Do not use them in the same LaTeX file, as they may cause unexpected errors.
• Truth-table example (tex source, pdf file).
• Tableaux example (tex source, pdf file).

LaTeX has existed since the early 1980's, and is being constantly developed and refined by many groups in many different places on planet Earth. If the documents posted above do not give you enough for your purposes, you will always find dozens of manuals and guides by browsing the Web.