Logic and Proof:  2012-2013

Overview

Logic plays an important role in many disciplines, including Philosophy and Mathematics, but it is particularly central to Computer Science. This course emphasises the computational aspects of logic, including applications to databases, constraint solving, programming and automated verification, among many others.  We also highlight algorithmic problems in logic, such as SAT-solving, model checking and automated theorem proving. 

The course relates to a number of third-year and fourth-year options. Temporal logic is used extensively in Computer-Aided Formal Verification and Probabilistic Verification. Propositional and predicate logic are also central to Complexity Theory, Knowledge Representation and Reasoning and Theory of Data and Knowledge Bases.

Learning outcomes

At the end of the course students are expected to:

• Understand and be able to explain and illustrate the meaning of given logical formulas, to translate such formulas into English and vice-versa.
• Be able to use the resolution proof system in proposiitonal logic and in predicate logic.
• Be able to express and formalize in a logical language properties of models such as graphs, strings and transition systems, and be able to determine the truth or falsity of such formulas in a given model.

Synopsis

Propositional logic (7 Lectures).

1. Syntax of propositional logic.  Translating combinatorial problems to propositional logic.  Truth tables.
2. Validity and satisfiability of formulas.  Logical equivalence and algebraic reasoning.
3. Normal forms: CNF, DNF, Tseitin's encoding.
4. Compactness Тheorem.
5. Polynomial-time algorithms for Horn formulas and 2-SAT. 
6. Resolution: soundness and refutation completeness. 
7. The Davis-Putnam procedure. 

First-order logic (7 Lectures).

1. Signatures, structures and valuations. 
2. Examples: graphs, trees, strings, relational databases and number systems.
3. Formula evaluation on finite structures.
4. Prenex normal form and Skolemisation.
5. Herbrand models and ground resolution.
6. Unification and resolution for predicate logic.
7. Decidable theories.

Temporal Logic (2 lectures).

1. Linear Temporal Logic (LTL) and example specifications.
2. Semantics of LTL, including basic equivalences
3. Model checking LTL formulas by inspection.

Syllabus

• Introduction to propositional logic. Syntax of propositional logic. Truth tables. Resolution. Davis-Putnam procedure.  Notions of soundness and completeness. 
• Introduction to first-order logic. Syntax of first-order logic.  Semantics of first-order logic: graphs, strings, databases and number systems as first-order structures.
• Prenex form and Skolemisation.
• Herbrand models and ground resolution.  Unification and resolution for predicate logic.
• Decidable theories.
• Introduction to Linear Temporal Logic.  Kripke structures and model checking.

Reading list

Primary text:

• Logic for Computer Scientists.  Uwe Schoning.  Modern Birkäuser Classics, Reprint of the 1989 edition.

Secondary text:

• Logic in computer science: modelling and reasoning about systems,2nd edition, by M. Huth and M. Ryan (Cambridge University Press, Cambridge 2004).

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.