Schedule and Lecture Notes

Here 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
Readings:
Consistancy: 2003 Lec 5

Sept 16 Completeness of Tableau Lecture 7: pdf
Readings
Completeness: 2003 Lec 6
Sept 21 Compactness and SAT Solvers

Lecture 8: pdf
Readings:
Compactness: 2003 Lec 7
Davis Putnam Procedure
Resolution

 
Sept 23 Decidability, SAT, and NP Problems

Lecture 9: pdf
Supplemental
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
Proofs and Programs
Integer Square Root Example
Refinement Logic Examples
Nov 4 Verification examples, primitive recursive functions, Hoare while rule and iterative proofs, real-life verification

Lecture 20: pdf
Proof of Stamps Problem

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
General Recursive Functions

Nov 16

Computational semantics of propositional logic, the Brouwer-Heyting-Kolmogorov (BHK) semantics and the propositions as types principle, proof terms. Homework Assignment 7.

Lecture 23: pdf
Nov 18

Computational semantics of quantification theory, BHK semantics for quantifier, relationship to types, more proof terms. Quiz 3 on computational semantics

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
Supplemental: Intuitionistic Propositional Calculus

Dec 7    
Dec 9