Computational Logic

Bolzano, Spring '08

  Instructor:           David Toman (david@cs.uwaterloo.ca)   
  Office:               Post Office 228 (office hours by appointment)    
  Lectures/Exercises    Wed  8:30-10:30   E420
                        Wed 18:00-19:00   E431 

  Class Info:           http://db.uwaterloo.ca/~david/cl

Syllabus:

  • Objectives and Outcome:
    The objective of this course is to offer a comprehensive introduction of the methods and techniques in Computational Logic. Although the course has a formal background, it includes a strong practical part in using automated tools and with a review of applications.
  • Basic Info:
    Credits: 4 (24 lectures, 12 exercises, all in English)
    Assessment: written final exam (July 11, 4:30p.p. in E221), project
  • Lectures/Exercises:

    1. Introduction: Models and Proofs, Completeness, Standard Theorems
    2. Tableaux (definition, properties), Complexity of proofs (survey, complexity of tableaux)
    3. Resolution up to SLD (resolution, SLD-resolution)
    4. DPLL ("Davis-Putnam") style approaches (abstract DPLL, original paper, and MiniSat)
    5. Natural Deduction (introduction); Intuitionistic Logic and type systems
    6. Modal and Temporal Logics (Rajev Gore's Modal Tableaux Methods [pages 1-10 for background])
    7. Tableaux Revisited (paper above, section 6 for modal logics, for LTL)
    8. Automata Techniques (Automata and Logic, From Logics to Algorithms)
    9. First order logic: Completeness, Compactness, (and incompleteness), Proof systems (Wilfrid Hodges' intro to FOL)
    10. Resolution for FOL
    11. Adding "interpreted theories": SAT Modulo Theories, Constraint Logic Programming, and Equational reasoning w/Paramodulation

  • Project:

    Write a survey of one of the topics covered in class (e.g., a survey on the use of the tableaux approach for propositional logic). The survey should recapitulate the material presented in class, compile a list of relevant references to literature (e.g., papers where the technique was first proposed, where major improvements were proposed, classical textbooks covering the topic, etc.). Moreover, the survey should contain a list of major results and outlines of proofs. Optionally, a sample "proof-of-concept" implementation (in particular for the propositional techniques) can be used as a part of the survey to illustrate various salient points of the technique and/or optimizations possible. The survey should be about 12-15 pages long (note that this is very little space, so you will need to think about how to present the material concisely).