CSE-433 Logic in Computer Science - Schedule
[ Home
| Schedule
| Assignments
| Software
| Resources
| Students
]
gla@postech Sungwoo Park
- The schedule is subject to change throughout the semester.
- CS = Course Notes.
(The up-to-date version including all chapters
[PS, PDF])
| Date |
Lecture |
Reading |
Quiz and Assignment Due |
|
| Tue | Sep | 4 | |
Judgments, Inference rules, Inductive proofs
(No class - Inauguration ceremony. To be rescheduled: 10am, Sep 7, in the classroom) |
CSE-321 Programming Languages Course Notes Chapter 2
[PS,
PDF]
|
|
| Thu | Sep | 6 | |
Inductive proofs, Overview of logic |
|
|
|
| Thu | Sep | 11 | |
Propositions, Propositional logic, Natural deduction |
CS Chapter 1 [PS, PDF]
On the Meaning of the Logical Constants and the Justification of the Logical Laws, Martin-Löf
[HTML]
Truth of a Proposition, Evidence of a Judgement, Validity of a Proof, Martin-Löf
[PDF]
|
Quiz 1
[PS,
PDF ]
|
| Thu | Sep | 13 | |
Notational definition, Logical equivalence
|
class-1.v |
Assignment 1 |
|
| Tue | Sep | 18 | |
Hypothetical judgments, Substitution principle, Structural properties |
|
|
| Thu | Sep | 20 | |
Local soundness and completeness, Proof reduction and expansion |
|
Assignment 2 |
|
| Tue | Sep | 25 | |
(No class - Chusok)
|
|
|
| Thu | Sep | 27 | |
Normal proofs, Normalization |
|
|
|
| Tue | Oct | 2 | |
Curry-Howard isomorphism
(Instructor out of town. To be rescheduled: 11:45am, Sep 28, in the classroom)
|
CS Chapter 2 [PS, PDF]
|
|
| Thu | Oct | 4 | |
Properties of proof terms
|
|
Assignment 3 |
|
| Tue | Oct | 9 | |
First-order logic - Introduction |
CS Chapter 3 [PS, PDF]
|
Quiz 2
[PS,
PDF ]
|
| Thu | Oct | 11 | |
First-order logic - Quantifications |
|
|
|
| Tue | Oct | 16 | |
First-order logic - Soundness and completeness |
|
Assignment 4 |
| Thu | Oct | 18 | |
First-order logic - Proof terms |
|
|
|
| | | |
Midterm,
Oct 25 (Thursday), 10am - 1pm, classroom. Closed book.
Exam [PS, PDF]
Solution [PS, PDF]
|
Assignment 5
(Oct 23)
|
|
| Tue | Oct | 30 | |
Introduction to datatypes |
CS Chapter 5 [PS, PDF]
| |
|
| Thu | Nov | 1 | |
Primitive recursion |
|
|
|
| Tue | Nov | 6 | |
Predicate on terms |
|
|
| Thu | Nov | 8 | |
Induction on terms |
|
|
|
| Tue | Nov | 13 | |
Proof terms |
|
| Thu | Nov | 15 | |
Examples of induction |
|
|
| Tue | Nov | 20 | |
Induction on predicates |
|
Assignment 6 |
| Thu | Nov | 22 | |
Examples of induction on predicates |
|
|
|
| Tue | Nov | 27 | |
Definitional equality |
|
Assignment 7 |
| Thu | Nov | 29 | |
Classical logic
(Instructor out of town. To be rescheduled: 7:00pm, Dec 12, in the classroom)
| )
CS Chapter 6 [PS, PDF]
| |
|
| Tue | Dec | 4 | |
CPS transformation |
|
Assignment 8 |
| Thu | Dec | 6 | |
Linear logic (I) |
Chapters 1 and 2 of Course Notes
by Frank Pfenning
| |
|
| Tue | Dec | 11 | |
Linear logic (II) |
|
|
| Thu | Dec | 13 | |
Review |
|
|
|
| | | |
Final Exam
Dec 18 (Tuesday), 7pm - 10pm (3 hours). Closed book.
Engineering building 109 (°øÇÐ2µ¿ 109È£)
Exam [PS, PDF]
Solution [PS, PDF]
|
[ Home
| Schedule
| Assignments
| Software
| Resources
| Students
]
gla@postech Sungwoo Park
|