Computational Logic
CS 7480 Fall 2010

College of Computer and Information Science
Northeastern University

Tentative Syllabus

Here is an overview of the material that I would like to cover. I reserve the right to make modifications based on the interests of the class and/or time constraints.
  1. Propositional Logic
    • Syntax, semantics & theories
    • Compactness
    • Complexity: hardness results & efficiently decidable cases, including 2SAT & HORNSAT
    • BDDs (Boolean Decision Diagrams)
    • Davis-Putnam-Loveland-Logemann SAT algorithm
  2. First-Order Logic
    • Syntax, semantics & model theory for FOL
    • Proof theory & its soundness
    • Completeness of FOL
    • Compactness, Lowenheim-Skolem, & related theorems
    • FOL as the foundations of mathematics
    • Undecidability of FOL & arithmetic
    • Godel's incompleteness theorems
  3. Decision Procedures
    • Uninterpreted functions & equality
    • Presburger arithmetic
    • Linear arithmetic
    • Combining decision procedures with SMT
  4. ACL2 (A Computational Logic for Applicative Common Lisp)
    • The ACL2 programming language
    • The ACL2 logic, recursion and induction
    • Effective use of the ACL2 theorem prover & applications
    • Selected topics in mechanized reasoning