Syllabus

Software

• LaTeX style file, proof.sty, for typesetting proof trees
• LaTeX Example file for using proof.sty
• User manual for the otter theorem proving system

Wetware

• Josh Hodas (Professor)
• Rett Bull (Professor)

Professor Bull's Notes from Fall 2000

Lectures Slides:

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

Programming Projects

• Project #1 -- Propositional Logic: Implementing Resolution - Conversion to CNF (Due Friday, March 30)
• Project #2 -- Propositional Logic: Implementing Resolution - Resolution (Due Monday, April 16)
• Project #3 -- Fun with otter (Due Monday, April 30)

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

Missing Figure for Midterm 1