CS 4860 |
Applied Logic |
Fall 2010 |
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 |
Aug 26 | Story of Logic | Lecture 1: pdf Readings: Begriffsschrift and Writing Programs |
Aug 31 | Story of Logic and Foreward on Trees (See lecture 1 and lecture 3) |
Lecture 2: pdf Readings: First Order Logic |
Sept 2 | Trees and Formulas | Lecture 3: pdf |
Sept 7 |
|
Lecture 4: pdf |
Sept 9 | Formulas and Boolean Valuations | Lecture 5: pdf |
Sept 14 | Consistency of Tableau | Lecture 6: pdf |
Sept 16 | Completeness of Tableau | Lecture 7: pdf Readings Completeness: 2003 Lec 6 |
Sept 21 | Compactness and SAT Solvers | Lecture 8: pdf
|
Sept 23 | Decidability, SAT, and NP Problems | Lecture 9: pdf |
Sept 28 | Lecture 10: pdf |
|
Sept 30 | Introduction to First-Order Logic | Lecture 11: pdf Quiz 1 |
Oct 5 | Syntax of First-Order Logic | Lecture 12: pdf |
Oct 7 | Semantics of First-Order Logic (models, satisfiability, validity) and Tableau Proofs | Lecture 13: pdf |
Oct 12 | *FALL BREAK* | |
Oct 14 | Completeness of First-Order Logic | Lecture 14: pdf |
Oct 19 | First-Order Completeness, Model Checking |
Lecture 15: pdf |
Oct 21 | Non-standard Models, Open Problem on Tableau Search | Lecture 16: pdf |
Oct 26 | Block Tableau, Gentzen Systems | Lecture 17: pdf Handout Lecture 18: pdf |
Oct 28 | Gentzen Systems | Lecture 18: pdf Handout Lecture 19: pdf |
Nov 2 | Refinement Logic for Integers and Lists |
Lecture 19: pdf |
Nov 4 | Verification examples, primitive recursive functions, Hoare while rule and iterative proofs, real-life verification | Lecture 20: pdf |
Nov 9 | Verification examples, primitive recursive functions, Hoare while rule and iterative proofs, real-life verification examples continued |
Lecture 21: pdf |
Nov 11 | Partial recursive functions, lambda terms, unsolvable problems, and Godel's incompleteness theorem, Quiz 2 on induction |
Lecture 22: pdf |
Nov 16 | Lecture 23: pdf | |
Nov 18 | Lecture 24: pdf | |
Nov 23 | Guest lecture on interactive proof assistants if requested. Thanksgiving break starts Nov. 24. |
Lecture 25: |
Nov 25 | *THANKSGIVING BREAK* | |
Nov 30 | Event Logic and reasoning about protocols. Quiz 4 (final quiz) on proof terms | Lecture 26: Semantics of Evidence |
Dec 2 | Summary of course, more of the Story of Logic and review of major concepts |
Lecture 27: Godel's Incompleteness Theorem |
Dec 7 | ||
Dec 9 |