INF 585: Logics for Computer Science: SPRING 2006

[Contents: instructors / venue / overview / grading / notes / outline / web resources / projects ]

Instructors

Two instructors will share the teaching of this course: Jean-Pierre Jouannaud and Dale Miller.

Venue and Dates

During Spring 2006, all classes are held in PC n° 41 during 13h45 - 17h30 on the following dates: Wednesday 4 Jan and Monday (for all the remaining classes) 9 Jan, 23 Jan, 30 Jan, 6 Feb, 27 Feb, 13 Mar, 20 Mar, and 27. Mar

Overview

Logic plays both a foundational role and common tool in computer science. It's role is similar to that of mathematics in physics. This course will present first-order and equational logics. The foundational material will deal with the the notions of truth and proof and the basic theorems of soundness and completeness that connects the them. The notion of proof will be analyzed in detail to uncover means to automate aspects of theorem proving. Programming tasks and some popular computer tools will be used to illustrate some of the many ways that logic can be applied to computer science problems.

Note: This course is for "Majeure 2". If you are planning to do a masters in MPRI (Mastère Parisien de Recherche en Informatique), you will need some background in formal logic. This course is designed, in part, to provide such background.

Grading of Students

We plan to evaluate students as follows:

  1. Project: Each student will need to choose a project in collaboration with the instructors so that there will not be any overlap. We expect these projects to require one or two days of work and will involve a simple implementation project in a high-level language or a software system (such as Maude). A list of projects will be made available.
  2. Oral exam: An oral exam will be given at the end of the class to test students understanding of the course material.

Lecture Notes

Lecture notes for Miller's first four lectures will be provided in class. Those notes are also available here.

Outline of Lectures

The following is a rough outline of what should be covered in 2006.

  1. Introduction: Motivation: roles of logic in computer systems; Specification of properties, correctness: Examples: verification of software, model checking, debugging (with assertions), correctness of security protocols, proof carrying code, ... ; Computation using logic: Functional programming (proof normalization, rewriting), Logic programming (proof search). ; Computer mathematics: Formalized mathematics, computer algebra ; Syntax of quantificational formulas. Propositional logic, models, normal forms. [4 Jan, dam]
  2. Proof Systems: Sequent calculus: 2 sided sequent. Lots of examples and lots of intuition about meaning of inference rules. [9 Jan, dam]
  3. Proofs and Truth: Soundness and completeness. ; Compactness, independence results. [23 Jan, dam]
  4. Meta-theory of Proof Systems: Cut-elimination: in-lining of lemmas ; Aspects of automation: decidability of tautologies; quantifiers make logic undecidable because the number of instances are quantifiers cannot be bounded. Various decidable fragments. ; Incompleteness theorem. [30 Feb, dam]
  5. Structures (Models): General definition for quantificational logic formulas. Evaluation in models; more axioms means fewer models. Consistency of theories with models. [6 Feb, jpj]
  6. Unification: Outline implementation of proof search with unification. ; Substitutions, more general substitutions. ; Unification given via transformation rules. ; Meta-properties: termination, complexity, MGU. [27 Feb, jpj]
  7. Horn clauses: Equivalence of three approaches: Sequent systems using Horn clauses, minimal model, inductive definitions. ; A general foundation for logic programming. ; Examples of Horn clause programming; Prolog introduced. [13 Mar, jpj]
  8. Equational logic: Tree structured proofs over one predicate. ; Refinement of models into algebras. ; Completeness a la Birkhoff. ; Rewriting: Confluence check, deduction in equational logic, computation as in functional programming. [20 Mar, jpj]
  9. Application of logic: Hoare logic and verification: Classical logic applied to verification. ; Rules of inference as structural recursion. ; Focus on the role of invariants and the need for additional data structures in logic (integers, lists, etc). [27 Mar, dam & jpj]

References and Web Resources

  1. Finite semantic trees suffice for resolution and paramodulation strategies, by Jean Goubault-Larrecq and Jean-Pierre Jouannaud (PDF).
  2. Rewrite Systems, by Nachum Dershowitz and Jean-Pierre Jouannaud. Handbook of Theoretical Computer Science, North-Holland, 1990.
  3. Both GNU Prolog and SWI-Prolog can be used for this class. They are available for free download and works on a number of computer platforms. Other Prolog implementations are also available and can be used, if desired. Most Prolog implementations differ, but they mostly support the core set of functionalities that we shall need in this class.
  4. There is a lot of information and tutorials on Prolog on the web. For example, a tutorial and an on-line guide. This latter site also seems to have a Java-based interpreter for Prolog that allows you to run Prolog in your browser.
  5. Logic for Computer Science: Foundations of Automatic Theorem Proving, by Jean Gallier, Wiley, pp. 511 (1986). This book is now out of print but available for free download.
  6. Two short articles: A Brief History of Logic and On the Unusual Effectiveness of Logic in Computer Science by Moshe Vardi.
  7. Some expository writing of Miller that may be of interest for students in this class.
    1. Logic and Logic Programming: a personal account. Also available as DVI and PDF.
    2. Proof Theory as an Alternative to Model Theory. Argues that the theory of proofs should also be considered a foundations for the design and justification of logic programming.
    3. Logic, Higher-order, by Dale Miller. A short article for the Encyclopedia of Artificial Intelligence: Second Edition, edited by S. Shapiro, 1992. (DVI, PDF).