Syllabus

Software

• LaTeX style file, proof.sty, for typesetting proof trees
• LaTeX Example file for using proof.sty
• SML Resources (lecture notes, practice assignments), etc.

Wetware

• Josh Hodas (Professor)

Professor Bull's Notes from Fall 2000

Lectures Slides (note, lecture #s correspond to 50 minute lectures):

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

Programming Projects

• Project #1 -- Propositional Logic: Implementing Resolution - Conversion to CNF (Due Monday, April 1)
• Project #2 -- Propositional Logic: Implementing Resolution - Resolution (Due Friday, April 19)
• Project #3 -- Fun With Otter (Due Wednesday May 8 [Automatic No-Penalty Extension to Friday May 10])
• 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 Thursday, May 16 [no late submissions])

Sample Solutions

• Solution to Homework 01
• Solution to Homework 02
• Solution to Homework 03
• Solution to Homework 04
• Solution to Homework 05
• Solution to Homework 06
• Solution to Homework 07