Schedule

• Thu, Jan 19:  Syntax of propositional logic, Handout 01. Natural deduction in propositional logic, Handout 02, Reading: [LCS, Sections 1.2 and 1.3].   Examples of natural deductions (tex source, pdf file). Lecture scribe: Sean Smith, lecture notes (tex source, pdf file).
  Assignment 1 and solutions (pdf, pdf), posted Jan 20, due Mon Jan 30.
• Tue, Jan 24:  Formal semantics of propositional logic, Handout 03. Classical versus intuitionistic propositional logic, Handout 04. Reading: [LCS, Section 1.3, 1.4],  Lecture scribe: Qi Wang, lecture notes (tex source, pdf file).
• Thu, Jan 26:  Soundness, compactness, completeness for propositional logic, Handout 05. Lecture scribe: Snehal Pandit, lecture notes (tex source, pdf file).
• Tue, Jan 31:  More on soundness, compactness, completeness for propositional logic, Handout 06. Lecture scribe: Yinghao Wang, lecture notes (tex source, pdf file).
  Assignment 2 and solutions (pdf, pdf), posted Jan 31, due Wed Feb 08.


• Thu, Feb 02:   Natural-deduction proofs versus truth-tables Handout 08. Universe of propositional WFF's Handout 07. Lecture scribe: Qi Wang, lecture notes (tex source, pdf file).
• Friday, February 03:  Project proposal due (pdf file of no more than 1-page, not graded).
• Tue, Feb 07:  Analytic tableaux, Handout 09. Normal forms of propositional logic, Handout 10. Lecture scribe: Tianying Zhang, lecture notes (tex source, pdf file).
  Assignment 3 and solutions (pdf, pdf), posted Feb 07, due Wed Feb 15.
• Thu, Feb 09:  Resolution in propositional logic, Handout 11. (Lecture cancelled because of snow storm.)
• Tue, Feb 14:  SAT solvers, Handout 12. Lecture scribe: Tian Zhang, lecture notes (tex source, pdf file).
  Assignment 4 and solutions (pdf, pdf), posted Feb 14, due Wed Feb 22.
• Thu, Feb 16:  Quantified Boolean formulas, Handout 13. Lecture scribe: Geng Lan, lecture notes (tex source, pdf file).
• Tue, Feb 21:  NO LECTURE. Monday schedule.
  Assignment 5 and solutions (pdf, pdf), posted Feb 21, due Wed Mar 01.
• Thu, Feb 23:  Continuation of quantified Boolean formulas (QBF's). . Lecture scribe: Benjamin Lawson, lecture notes (tex source, pdf file).
• Tue, Feb 28:  Binary decision diagrams (BDD's), Handout 14. Lecture scribe: Shravan Kumar, lecture notes (tex source, pdf file).


• Thu, Mar 02:   Binary decision diagrams (BDD's) continued. .
  Take-home MidTerm exam and solutions (tex, pdf, pdf), posted Mar 02 at 5:00 pm, due Mar 03 by 11:59 pm.


• Saturday, March 04 -- Sunday, March 12:  SPRING RECESS.


• Tue, Mar 14:   First-order logic, syntax Handout 15, proof rules Handout 16, semantics Handout 17, examples of first-order theories Handout 18.
  Assignment 6 and solutions (pdf, pdf), posted Mar 14, due Wed Mar 22.
• Thu, Mar 16: The same handouts posted on March 14, Reading: [LCS, Sections 2.2, 2.3, 2.4] for back up. Lecture scribe: Sean Smith, lecture notes (tex source, pdf file).
• Tue, Mar 21: Prenex normal form, Skolemization, Handout 19. Lecture scribe: Justin Chen, lecture notes (tex source, pdf file).
• Thu, Mar 23:  Algebraic and relational structures, Handout 20. Lecture scribe: Desheng Zhang, lecture notes (tex source, pdf file).
  Assignment 7 and solutions (pdf, pdf), posted Mar 23, due Fri Mar 31.
• Tue, Mar 28:  Soundness and completeness of first-order logic, Handout 21, first-order definability, Handout 22. Lecture scribe: Yinghao Wang, lecture notes (tex source, pdf file).
• Thu, Mar 30:  Examples of first-order definability, Handout 23, deductive closures, Handout 24. Lecture scribe: Rawane Issa, lecture notes (pdf file).
  Assignment 8 and solutions (pdf, pdf), posted Mar 30, due Fri Apr 07.


• Tue, Apr 04:  More on Herbrand theory and Gilmore's algorithm, Handout 25. Lecture scribe: Johnson Lam, lecture notes (tex source, pdf file).
• Thu, Apr 06:  Tableaux for first-order logic (part 1), Handout 26. Lecture scribe: Rawane Issa, lecture notes (pdf file).
  Assignment 9 and solutions (pdf, pdf), posted Apr 07, due Fri Apr 14.
• Tue, Apr 11:  Unification, Handout 27, Tableaux for first-order logic (part 2), Handout 28.
• Thu, Apr 13:  First-order resolution, Handout 29, Lecture scribe: Rawane Issa, lecture notes (pdf file).
  Assignment 10 and solutions (pdf, pdf), posted Apr 14, due Fri Apr 21.
• Tue, Apr 18:  Limits of formal modeling in propositional logic and first-order logic, Handout 30, Lecture scribe: Tian Zhang, lecture notes (pdf file).
• Thu, Apr 20:  SMT solvers, Handout 31.
  Assignment 11 and solutions (pdf, pdf), posted Apr 21, due Fri Apr 28.
• Tue, Apr 25:  Second-order logic, Handout 32, satisfiability modulo DL, Lecture slides (courtesy of Albert Oliveras).
• Thu, Apr 27:  Second-order logic (continued), Handout 33. Lecture scribe: Sean Smith, lecture notes (pdf file).


• Tue, May 02:  Program schemes and first-order logic, Handout 34.


• Thursday, May 04: Friday, May 05:  Term project due.
• Take-home end-of-term exam and solutions ( pdf, pdf), posted Tuesday, May 09, at 12:00 noon, due Wednesday, May 10 by 12:00 noon.