|
May 9
|
What is logic? Logic propositions and connectives.
|
[
Logic 01
|
Lu 2.1
|
F1
|
Z1
]
|
|
|
May 11
|
Truth tables; translations between English and propositional logic; propositional logic formulas; review of induction.
|
[
Logic 02
|
Lu 1.2, 2.2
|
F2
|
Z2
]
|
|
|
May 12
|
No tutorial
|
[
T1
]
|
Assignment 1
out
May 15
|
|
May 16
|
Structural induction; propositional language semantics; satisfiability.
|
[
Logic 03
|
Lu 2.3, 2.4
|
F3
|
Z3
]
|
|
|
May 18
|
Tautological consequence; proving arguments valid in propositional logic.
|
[
Logic 03
|
Lu 2.5
|
F4
|
Z4
]
|
|
|
May 19
|
Tutorial
|
[
T2
]
|
Assignment 1
due May 22
|
|
May 23
|
No lecture: May 23 follows a Monday schedule
|
|
|
|
May 25
|
Propositional calculus laws; disjunctive and conjunctive normal forms.
|
[
Logic 04
|
Lu 2.7
|
F5
|
Z5
]
|
|
|
May 26
|
Tutorial
|
[
T3
]
|
|
|
May 30
|
Adequate set of connectives; Boolean algebra; logic gates.
|
[
Logic 05
|
Lu 2.8
|
F6
|
Z6
]
|
|
|
June 1
|
Circuit design and minimization; code analysis and simplification.
|
[
Logic 05
|
F7
|
Z7
]
|
|
|
June 2
|
Tutorial
|
[
T4
]
|
Assignment 2
out
June 5
|
|
June 6
|
Formal deduction for propositional logic.
|
[
Logic 06
|
Lu 2.6
|
F8
|
Z8
]
|
|
|
June 8
|
Soundness and completeness of formal deduction for propositional logic (proof of completeness optional).
|
[
Logic 06
|
Lu 2.6
|
F9
|
Z9
]
|
|
|
June 9
|
Tutorial
|
[
T5
]
|
Assignment 2
due June 12
|
|
June 13
|
Automated theorem proving: resolution, Davis-Putnam procedure (proof of completeness of DPP optional).
|
[
Logic 07
|
F10
|
Z10
]
|
|
|
June 15
|
No lecture: self study for midterm
|
|
Midterm
on June 15
|
|
June 16
|
No tutorial
|
[
T6
]
|
|
|
June 20
|
First-order logic: domain, terms, relations, variables, quantifiers; translations from English to first-order logic.
|
[
Logic 10
|
Lu 3.1
|
F12
|
Z12
]
|
|
|
June 22
|
First-order logic syntax and semantics.
|
[
Logic 11
|
Logic 12
|
Lu 3.2, 3.3
|
F13
|
Z13
]
|
|
|
June 23
|
Tutorial
|
[
T7
]
|
Assignment 3
out
June 26
|
|
June 27
|
Logical consequence in first-order logic.
|
[
Logic 13
|
Lu 3.4
|
F14
|
Z14
]
|
|
|
June 29
|
Formal deduction in first-order logic.
|
[
Logic 14
|
Lu 3.5
|
F15
|
Z15
]
|
|
|
June 30
|
Tutorial
|
[
T8
]
|
Assignment 3
due July 4
|
|
July 4
|
Formal deduction in first-order logic: more proof examples, soundness and completeness.
|
[
Logic 14
|
Lu 3.5
|
F16
|
Z16
]
|
|
|
July 6
|
Resolution for first-order logic: prenex normal form, existential-free PNF, unification and resolution.
|
[
Logic 15
|
Lu 3.6
|
F17
|
Z17
]
|
|
|
July 7
|
Tutorial
|
[
T9
]
|
Assignment 4
out
July 10
|
|
July 11
|
Resolution for first-order logic: proof examples. Computation and logic: the satisfiability problem, the halting problem.
|
[
Logic 15
|
Logic 16
|
F18
|
Z18
]
|
|
|
July 13
|
Turing machines; computability and decidability.
|
[
Logic 16
|
F19
|
Z19
]
|
|
|
July 14
|
Tutorial
|
[
T10
]
|
Assignment 4
due July 17
|
|
July 18
|
Proving decision problems undecidable by reduction.
|
[
Logic 16
|
F20
|
Z20
]
|
|
|
July 20
|
Peano arithmetic; proving theorems in Peano arithmetic.
|
[
Logic 17
|
F21
|
Z21
]
|
|
|
July 21
|
Tutorial
|
[
T11
]
|
Assignment 5
out
July 24
|
|
July 25
|
Gödel's incompleteness theorem. Program verification: Hoare triples, partial and total correctness.
|
[
Logic 17
|
Logic 20
|
F22
|
Z22
]
|
|
|
July 27
|
Program verification: rules for assignment, implication, and composition, conditional statements.
|
[
Logic 20
|
F23
|
Z23
]
|
|
|
July 28
|
Tutorial
|
[
T12
]
|
Assignment 5
due July 31
|
|
Aug 1
|
Program verification: partial-while, program termination, undecidability of partial and total correctness.
|
[
Logic 20
|
F24
|
Z24
]
|
Final exam
on August 11
|