CS 81: Computability and Logic
Spring 2014

Course Staff and Consulting Hours (To be Announced)

 

For quickest response, please use our piazza site.

Submission site for homework

 

Grading Breakdown

 

Required Textbooks

• Richard Bornat, Proof and Disproof in Formal Logic: An Introduction for Programmers, Second Edition (Paperback), Oxford University Press (2005), ISBN-10: 0198530277 ISBN-13: 978-0198530275

• Michael Sipser, Introduction to the Theory of Computation, Third Edition (Hardcover), Course Technology (July, 2012), ISBN-10: 0534950973, ISBN-13: 978-0534950972
  Errata

 

Assignments

1. Assignment 1  
2. Assignment 2  
3. Assignment 3  
4. Assignment 4  
5. Assignment 5  
6. Assignment 6  
7. Assignment 7  
8. Assignment 8  
9. Assignment 9  
10. Assignment 10  
11. Assignment 11  

Lecture Slides

1.     Introduction, Propositional Logic, Part 1, Truth Tables

2.    Propositional Logic, Part 2, Tableaux, Natural Deduction

3.    Converting (Propositional) Tableaux to (Classical) Natural Deduction

4.    Predicate Logic

    More Jape Examples

5.    Predicate Logic, Part 2

6.    Propositional Soundness and Completeness

7.    Completeness Theorem Proof

8.    Predicate Tableaux

9.    Resolution Theorem Proving

10.    Program Logic

    "An Early Program Proof by Alan Turing"

11.    Computability Models, Finite-State Machines

    Classroom smartboard Monday 31 March 2014

    Classroom smartboard Wednesday 2 April 2014

    NFA to DFA worked examples

    Classroom smartboard Monday 7 April 2014

12.    Regular Expressions

13.    Product Machines

14.    State Equivalence

    Classroom smartboard Wednesday 9 April 2014

15.    Pumping Lemma for Regular Languages

16.    Myhill-Nerode Theorem, State Equivalence, and DFA Minimization

17.    Derivatives of Regular Expressions, Pattern-Matching

    Classroom smartboard Monday 14 April 2014

18.    Grammars

19.    Conversion to Chomsky Normal Form

    cfg2cnf.pro: Prolog code showing conversion of a CFG to Chomsky Normal Form

    Classroom smartboard Wednesday 16 April 2014

20.    Pushdown Automata

    FA and PDA Simulator: pflap.pro (version 0.7)

    Classroom smartboard Monday 21 April 2014

21.    Effective Computability

22.    Uncomputability

22.    (Some of) What You Need to Know About Computability and Uncomputability

    Classroom smartboard Monday 28 April 2014

23.    Reduction

Other Items of Interest

·      JAPE Distribution (Just Another Proof Editor)

·      Some Proofs of Interest

·      Using Lemmas in JAPE

·      Propositional tableau construction and tautology checker in Prolog

·      Propositional natural deduction prover in Prolog

·      Interpretation of predicate logic terms and formulas over a finite domain

·       LaTex Formatting Packages for proof boxes and more

• Set from Alan Davidson, HMC '06
• Set from Huth & Ryan (includes trees)
• Set from Paul Taylor
• bussproofs.sty
• LaTeX for Logicians
• GasTeX for Graph and Automata Drawing (JasTeX, GUI for producing GasTeX)
• ProofCheck: Proof Checker for LaTeX Proofs (video, from ProofCheck.org)
  
• TikZ Automata Drawing

 

• Prover9 Automatic Theorem Prover


• JFLAP (Java Formal Languages and Automata Package)