Syllabus

Software

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

Wetware

• Josh Hodas (Professor)

Professor Bull's Notes from Fall 2000

Lectures Slides:

• Introduction:
  • 01 (9/5, 9/7) Introduction, History, and Administrivia
• Mathematical Preliminaries:
  • 02 (9/7) Sets, Pairs, Products, and Relations
  • 03 (9/10, 9/12) Equivalence Relations, Orders, and Functions
  • 03a (9/12) Pairs redux
  • 04 (9/14, 9/17) Orders, LUBs & GLBs, Well-Founded Sets
  • 05 (9/17, 9/19) Principle of Complete Induction
• Propositional Logic:
  • 06 (9/19, 9/21) Syntax and Semantics
  • 07 (9/24, 9/26) Satisfiability, Validity, and Consequence
  • 08 (9/26, 9/28) Logical Equivalence, Substitution, Useful Equivalences
  • 09 (9/28, 10/1) Complete Sets of Connectives, Applications
  • 10 (10/3, 10/5) Decision and Deduction, Natural Deduction
  • 11 (10/8, 10/12) Sidebar on Intuitionistic (Constructive) Logics and Pierce's Formula, Classical Natural Deduction
  • 12 (10/15) Gentzen Sequent Calculus
  • 13 (10/17) Gentzen Sequent Calculus, Pierce's Formula
  • 14 (10/19, 10/24) CNF, The Resolution Rule and Procedure
  • 15 (10/24,10/26) Pre-Optimizations of Resolution
• Predicate Logic:
  • 16 (10/31) Syntax
  • 17 (11/2, 11/5) Applications - Mathematics
  • 18 (11/7,11/9) Applications - Databases
  • 19 (11/12) Applications - Databases
  • 20 (11/14) Semantics, Satisfiability, Validity, and Consequence, Useful Equivalences
  • 21 (11/16) Substitution
  • 22 () Natural Deduction
  • 23 () Gentzen Sequent Calculus
  • 24 () Towards First-Order Resolution: PCNF, Clausal Form
  • 25 () Towards First-Order Resolution: Skolemization, Herbrand Universe and Base
  • 26 () Towards First-Order Resolution: Herbrand's Theorem
  • 26a () Towards First-Order Resolution: Proof of Preliminary to Herbrand's Theorem
  • 27 () First-Order Resolution: Unification, Resolution Rule, Lifting Lemma
  • 28 () First-Order Resolution: Implementation Hints, Examples
  • 29 () Resolution -- Complete and Incomplete Heuristics. Horn Clauses
  • 30 () 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 Friday, September 21) (pdf, LaTeX)
• Homework 02 -- Propositional Logic: Syntax and Semantics (Due Friday, September 28) (pdf, LaTeX)
• Homework 03 -- Propositional Logic: Natural Deduction (Due Wednesday, October 10) (pdf, LaTeX)
• Homework 04 -- Propositional Logic: Gentzen Sequent Calculus (Due Friday, October 26) (pdf, LaTeX)
• Homework 05 -- Propositional Logic: Resolution Refutation and Matching (Due Friday, November 2) (pdf, LaTeX)
• Homework 06 -- Predicate Logic: Syntax, Semantics, and Encoding (Due 5, November 21) (pdf, LaTeX)
• Homework 07 -- Predicate Logic: Proof Theory (Due Wednesday, December 6) (pdf, LaTeX)

Programming Projects

• Project #1 -- Propositional Logic: Implementing Resolution - Conversion to CNF (Due Friday, November 16)
• Project #2 -- Propositional Logic: Implementing Resolution - Resolution (Due Friday, December 7)
• Optional Project #3 -- Fun With Otter (Due Saturday, December 22 [no late submissions])
• Optional Projects #4/#5/#6 -- First-Order Logic: Implementing Substitution and Unification (Project 4), Conversion to Clausal Form (Project 5), and Resolution (Project 6) (Due Saturday, December 22 [no late submissions])

Sample Solutions