FRAMES
NO
FRAMES
Schedule
- Tue, Sept 04:
truth-tables, DNF's, CNF's
(lecture slides 01),
syntax of PL
(lecture slides 02),
natural deduction in PL
(lecture slides 03).
- Thu, Sept 06:
formal modeling with PL
(lecture notes),
semantics of PL
(lecture slides 04), lecture scribe: Parul Sohal
(notes).
Assignment 1 and
solutions
(pdf,
pdf),
posted Sept 07, due Sept 14.
- Tue, Sept 11:
universe of PL wff's,
(lecture slides 05),
propositional wff's in special forms,
(lecture slides 06), lecture scribe: Ahmad Golchin
(notes).
- Thur, Sept 13:
completeness of PL proof rules,
(lecture slides 07),
soundness of PL proof rules,
(lecture slides 08),
de Morgan's laws once more,
(lecture slides 09), lecture scribe: Donghyun Kim
(notes).
Assignment 2 and
solutions
(pdf,
pdf),
posted Sept 14, due Sept 21.
- Tue, Sept 18:
analytic tableaux for PL,
(lecture slides 10), lecture scribe: Donghyun Kim
(notes).
- Thu, Sept 20:
resolution method for PL,
(lecture slides 11),
program unwinding,
(lecture slides 12),
lecture scribe: Konstantinos Sotiropoulos
(notes).
Assignment 3 and
solutions
(pdf,
pdf),
posted Sept 21, due Sept 28.
- Tue, Sept 25:
binary decision diagrams,
(lecture slides 13), more on BDD's by
Donald Knuth, click
here,
lecture scribe: Isidora Chara Tourni (notes).
- Thu, Sept 27:
quantified Boolean formulas (QBF's)
(lecture slides 14),
lecture scribe: Gavin Brown (notes).
Assignment 4 and
solutions
(pdf,
pdf),
posted Sept 28, due Oct 04.
- Tue, Oct 02:
syntax and proof rules of first-order logic
(lecture slides 15,
lecture slides 16 ),
lecture scribe: Jiayu Zhang (notes).
- Thu, Oct 04:
semantics of first-order logic
(lecture slides 17),
examples of first-order theories
(lecture slides 18),
lecture scribe: Laura Greige (notes).
Assignment 5 and
solutions
(pdf,
pdf),
posted Oct 05, due Oct 12.
- Tue, Oct 09:
MONDAY SCHEDULE, no lecture.
- Thu, Oct 11:
prenex normal forms
(lecture slides 19),
first-order structures
(lecture slides 20),
lecture scribe: Parul Sohal (notes).
Assignment 6 and
solutions
(pdf,
pdf),
posted Oct 12, due Oct 19.
- Tue, Oct 16:
soundness and completeness
(lecture slides 21),
first-order definability
(lecture slides 22).
- Thu, Oct 18:
extended example
(lecture slides 23),
further examples of first-order
definability
(lecture notes), lecture scribe: Andy Huynh
(notes).
Assignment 7 and
solutions
(pdf,
pdf),
posted Oct 19, due Oct 26.
- Tue, Oct 23:
deductive closures and first-order theories
(lecture slides 24).
- Thu, Oct 25:
reading assignment [LCS, pp 131-138] (not covered in handouts),
compactness and completeness
(lecture notes).
- Tue, Oct 30:
MidTerm Exam
and solutions
(pdf,
pdf).
- Thu, Nov 01:
program schemes and first-order logic
(lecture slides 25).
Assignment 8 and
solutions
(pdf,
pdf),
posted Nov 02, due Nov 09.
- Tue, Nov 06:
Gilmore's algorithm for first-order logic
(lecture slides 26).
- Thu, Nov 08:
tableaux for classical
first-order logic (part 1)
(lecture slides 27).
Assignment 9 and
solutions
(pdf,
pdf),
posted Nov 09, due Nov 16.
- Tue, Nov 13:
MaxSat and Bayesian networks
(lecture slides 28),
first-order unification
(lecture slides 29), lecture scribe:
Isidora Tourni
(notes)
- Thu, Nov 15:
tableaux for classical
first-order logic (part 2)
(lecture slides 30).
Assignment 10 and
solutions
(pdf,
pdf),
posted Nov 16, due Nov 28.
- Tue, Nov 20:
first-order resolution
(lecture slides 31),
introduction to abstract interpretation
(lecture slides 32).
- Wednesday, Nov 21 --
Sunday, Nov 25: THANKSGIVING RECESS.
- Tue, Nov 27:
limits of formal modeling in PL and FOL
(lecture slides 33).
- Thu, Nov 29:
limits of formal modeling in PL and FOL
(lecture slides 33), continued.
Assignment 11 and
solutions
(pdf,
pdf),
posted Nov 30, due Dec 07.
- Tue, Dec 04:
SAT solvers
(lecture slides 34).
- Thu, Dec 06:
SMT solvers
(lecture slides 35).
Assignment 12 and
solutions
(pdf,
pdf
),
posted Dec 07, due Dec 14.
- Tue, Dec 11:
second-order logic
(lecture slides 36).
Last lecture.
-
For course evaluation, use any portable smart device
(phone, tablet, laptop, etc.) and use your internet browser to go to
Course
Evaluations. Follow the instructions on the screen. Your evaluations
are anonymous and instructors will not receive the results before
all final grades are submitted.
- Wednesday, Dec 19:
End-of-Term Exam
and solutions
(pdf,
pdf).
posted Dec 16 at 12:00 noon, due Dec 20 by 12:00 noon.
Maintained by Assaf Kfoury
Created: 2018.08.05 Last modified:
2018.12.15