Skip to main content

Logic and Proof:  2015-2016

Lecturer

Degrees

Schedule S1(CS&P)(3rd years)Computer Science and Philosophy

Part A CoreComputer Science

Part AMathematics and Computer Science

Term

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.Propositional and predicate logic are central to Complexity Theory, Knowledge Representation and Reasoning, and Theory of Data and Knowledge Bases. They are also used extensively in Computer-Aided Formal Verification, Probabilistic Model Checking and Software Verification.

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 (8 Lectures).

  1. Introduction. History of mathematical logic in computer science.
  2. Syntax and semantics of propositional logic.  The SAT problem. Translating constraint problems to SAT.
  3. Logical equivalence and algebraic reasoning. CNF and DNF.
  4. Polynomial-time algorithms: Horn formulas, 2-SAT, WalkSAT, and XOR-clauses.
  5. Binary decision diagrams.
  6. Resolution: soundness and refutation completeness. 
  7. DPLL, clause learning, improvements, stochastic resolution.
  8. Compactness theorem.

First-order logic (8 Lectures).

  1. Signatures, structures and valuations. 
  2. Examples: graphs, trees, strings, relational databases and number systems.
  3. Prenex normal form and Skolemisation.
  4. Herbrand models and ground resolution.
  5. Unification and resolution for predicate logic.
  6. Undecidability of satisfiability.
  7. Decidable theories: dense linear orders and linear arithmetic over the natural numbers.

Syllabus

  • Syntax of propositional logic. Truth tables. 
  • Horn-SAT and 2-SAT.  
  • Binary decision diagrams.
  • Resolution. DPLL procedure. 
  • Compactness theorem.  
  • Syntax and semantics of first-order logic.  
  • Prenex normal form and Skolemisation.
  • Herbrand models and ground resolution.  
  • Unification and resolution for predicate logic.
  • Undecidability of satisfiability for first-order logic.  
  • Decidable theories, including linear arithmetic.

Reading list

Primary text:

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

Secondary texts:

  • Logic in computer science: modelling and reasoning about systems,2nd edition, by M. Huth and M. Ryan (Cambridge University Press, Cambridge 2004).
  • Mathematical Logic for Computer Science, 3rd edition, by M. Ben-Ari. Springer, 2012.

Feedback

Students are formally asked for feedback at the end of the course. Students can also submit feedback at any point here. Feedback received here will go to the Head of Academic Administration, and will be dealt with confidentially when being passed on further. All feedback is welcome.

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.