CS 4860 |
Applied Logic |
Spring 2009 |
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 20 | What is Logic? | Lecture 1: pdf Readings Begriffsschrift and Writing Programs |
| Jan 22 | Propositional Logic | Lecture 2: pdf Readings First Order Logic |
| Jan 27 | Proving Satisfiability & Validity |
Lecture 3: pdf |
| Jan 29 | Efficient SAT solving |
Lecture 4: pdf |
| Feb 3 | Lecture 5: pdf | |
| Feb 5 | Lecture 6: | |
| Feb 10 | Lecture 7: pdf Readings Propositional Resolution |
|
| Feb 12 | Lecture 8: | |
| Feb 17 | From Analytic Tableaux to Gentzen Systems Lecture | Lecture 9: pdf |
| Feb 19 | Gentzen Systems vs. Block Tableaux Lecture | Lecture 10: pdf Readings Blocked Tableau and Sequent Systems |
| Feb 24 | Refinement Logic Lecture | Lecture 11: pdf |
| Feb 26 | Consistency and Completeness of Refinement Logic | Lecture 12: pdf |
| Mar 3 | Second-Order Propositional Logic (Syntax, Substitution) | Lecture 13: pdf |
| Mar 5 | Second Order Propositional Logic (Semantics and Proof Rules) | Lecture 14: pdf |
| Mar 10 | First-Order Logic (Syntax and Semantics) | Lecture 15: pdf |
| Mar 12 | First-Order Tableaux | Lecture 16: pdf |
| Mar 17 | *SPRING BREAK* | |
| Mar 19 | *SPRING BREAK* | |
| Mar 24 | Correctness and Completeness of First-Order Tableaux | Lecture 17: pdf |
| Mar 26 | Undecidability and Compactness of First-Order Logic | |
| Mar 31 | Expressing Mathematical Concepts (I) | |
| Apr 2 | Expressing Mathematical Concepts (II) |
Lecture 20: pdf |
| Apr 7 | Axiomatizing Integer Arithmetic | |
| Apr 9 | Arithmetic Representability |
Lecture 22: pdf |
| Apr 14 | Unsolvable Problems in Logic |
Lecture 23: pdf |
| Apr 16 | The theory Q and the undecidability of logic |
Lecture 24: pdf |
| Apr 23 | Lecture 25 | Lecture 25: pdf |