Syllabus

Software

• LaTeX style file, proof.sty, for typesetting proof trees
• LaTeX Example file for using proof.sty

Wetware

• Josh Hodas (Professor)

Lectures

• 01 (09/01) Introduction, History, and Administrivia
• Mathematical Preliminaries:
  • 02 (09/03) Sets, Pairs, Products, and Relations
  • 03 (09/03-09/06) Relations, and Equivalence Relations, and Orders
  • 03a (09/06) Pairs redux
  • 04 (09/06-09/08) Orders, LUBs & GLBs, Well-Founded Sets
  • 05 (09/08) Principle of Complete Induction
  • 06 (09/10) Strings and Trees
  • 07 (09/13) Complete Discussion of Trees, Complexity of Ackermann's Function
• Propositional Logic:
  • 08 (09/15) Syntax and Semantics
  • 09 (09/17) Satisfiability, Validity, and Consequence
  • 10 (09/22) Logical Equivalence, Substitution, Useful Equivalences
  • 11 (09/24) Complete Sets of Connectives, Decision and Deduction
  • 12 (09/27) Hilbert Systems and The Deduction Theorem
  • 12a (09/29) Proof of The Deduction Theorem
  • 13 (09/29-10/01) Hilbert System -- Additional Derived Rules
  • 14 (10/01) Sidebar on Intuitionistic (Constructive) Logics and Pierce's Formula
  • 15 (10/04) Natural Deduction
  • 16 (10/06) Natural Deduction
  • 17 (10/11) Gentzen Sequent Calculus
  • 18 (10/13) Gentzen Sequent Calculus, Pierce's Formula
  • 19 (10/15) CNF, The Resolution Rule and Procedure
  • 20 (10/20) Predicate Logic: Pre-Optimizations of Resolution
• Predicate Logic:
  • 21 (10/22) Syntax
  • 22 (10/25) Applications - Mathematics
  • 23 (10/27) Applications - Mathematics
  • 24 (10/29) Applications - Databases
  • 25 (11/1) Applications - Databases
  • 26 (11/3) Semantics, Satisfiability, Validity, and Consequence
  • 27 (11/5) Substitution
  • 28 () Natural Deduction
  • 29 () Gentzen Sequent Calculus
  • 30 () Useful Equivalences (Ben-Ari, section 3.4), Towards First-Order Resolution: PCNF
  • 31 () Towards First-Order Resolution: Skolemization, Clausal Form (from 30), Herbrand Universe and Base
  • 32 () Towards First-Order Resolution: Herbrand's Theorem (from 31) and Proof.
  • 33 () First-Order Resolution: Unification, Resolution Rule, Lifting Lemma
  • 34 () First-Order Resolution: Implementation Hints, Examples
  • 35 () Resolution -- Complete and Incomplete Heuristics. Extending Horn Clauses
  • 36 () Extending Horn Clauses, Hereditary Harrop Formulas
• Hoare Logic
  • 37 () Key Concepts, Calculation of Weakest Precondition
  • 38 () Deduction System, Sample Partial Correctness Proof

Assignments

• Homework 01 -- Mathematical Preliminaries (Due Wednesday, September 15) (pdf)
• Homework 02 -- Lumberjacking (Due Thursday, September 23) (pdf)
• Homework 03 -- Propositional Logic: Syntax and Semantics (Due Wednesday, September 29) (pdf)
• Homework 04 -- Propositional Logic: Hilbert Systems (Due Wednesday, October 6) (pdf, LaTeX)
• Homework 05 -- Propositional Logic: Natural Deduction (Due Wednesday, October 13) (pdf)
• Homework 06 -- Propositional Logic: Gentzen Sequent Calculus (Due Wednesday, October 27) (pdf, LaTeX)
• Homework 07 -- Predicate Logic: Syntax, Semantix, and Encoding (Due Wednesday, November 17) (pdf, LaTeX)
• Homework 08 -- Predicate Logic: Proof Theory (Due Monday, December 6) (pdf, LaTeX)

Programming Projects

• Project #1 -- Propositional Logic: Implementing Resolution / Phase 1: Conversion to CNF (Due Thursday, November 11)
• Project #2/#3 -- Propositional Logic: Implementing Resolution / Phase 2 Subphase 1 and 2: Resolution (Due Tuesday, November 23 / Thursday, December 9 [no late submissions])-->
• Optional Projects #4/#5/#6 -- First-Order Logic: Implementing Substitution, Unification, Clausal Form, and Resolution (Due Tuesday, December 14 [no late submissions])-->

Sample Solutions

• Solution to Homework 01
• Solution to Homework 02
• Solution to Homework 03 Problem 1
• Solution to Homework 04 Problems 2-5
• Solution to Homework 05
• Solution to Homework 06