CS 6862 |
Applied Logic |
Spring 2011 |
Schedule and Lecture NotesHere is a list of the lectures planned for the course. Note that topics are subject to change. |
||
| Date | Topic | Lecture Notes and Readings |
| Jan 25 | Course Introduction, the story of logic
|
Lecture 1: pdf |
| Jan 27 | Ways of defining logics formally, recursive types | Lecture 2: pdf |
| Feb 1 | Boolean logics-- propositional, first order (FOL) |
Lecture 3: pdf |
| Feb 3 | Computational logics -- first order | Lecture 4: pdf |
Feb 8 |
Evidence semantics | Lecture 5: pdf |
| Feb 10 | Evidence semantics continued | Lecture 6: pdf |
| Feb 15 | Consistency and completeness issues | Lecture 7: pdf |
| Feb 17 | Types and sets | Lecture 8: pdf |
| Feb 22 | First-Order theories-- PA, HA | Lecture 9: pdf |
| Feb 24 | Peano Arith (PA) and Heyting Arithmetic (HA) | Lecture 10: pdf |
| Mar 1 | Godel translation of PA into HA | Lecture 11: pdf |
| Mar 3 | Markov's Principle | Lecture 12: pdf |
| Mar 8 | Marvov's Principle (MP) and Hoare While Rule | |
| Mar 10 | Consistency of Markov's Principle | Lecture 13: pdf |
| Mar 15 | Godel system T, higher-order functions |
Lecture 14: pdf |
| Mar 17 | Translating classical proofs to constructive proofs, Murthy results | Lecture 15: pdf Problem Set 3 |
| Mar 22 | **Spring Break** | |
| Mar 24 | **Spring Break** | |
| Mar 29 | Brouwer ordinals and W-types | Lecture 16: pdf |
| Mar 31 |
|
Lecture 17: pdf |
| Apr 5 | Kleene theorem on recursive fans, Continuity principles |
Lecture 18: |
| Apr 7 | Brouwer's Bar Theorem, Kleene realizability |
|
| Apr 12 | Martin-Lof's Intuitionistic Type Theory (ITT) |
|
| Apr 14 | Realizing Bar Induction |
Lecture 21: pdf |
| Apr 19 | Howe's computational equality and Howe's trick | Lecture 22: pdf |
| Apr 21 | Partial equivalence relation (per) semantics | |
| Apr 26 | Richer types -- dependent records |
|
| Apr 28 | Bar types and unsolvable problems | Lecture 25: pdf |
May 3 May 5 |
Process type Unsolvability without Church's Thesis (CT) |
Lecture 27: pdf |