Skip to main content

Logic and Proof:  2010-2011

Lecturer

Degrees

ModerationsComputer Science

Part AMathematics and Computer Science

Term

Overview

The main aim of the course is to give a first introduction to formal logic for computer scientists.

  • Introduction to propositional logic. Syntax of propositional logic. Truth tables. Sequent Calculus. Resolution. Notions of soundness and completeness. Proofs by induction on the structure of formulas.
  • Introduction to structures. Examples. Introduction to finite state transition systems.
  • Introduction to first-order logic. Syntax of first-order logic. Semantics of first-order logic. Game-based semantics. Examples. Sequent Calculus. Notions of soundness and completeness.Logic as database query language.
  • Introduction to temporal logics, especially Linear Temporal Logic (LTL). Examples.

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.
  • Construct simple, but rigorous, formal proofs for some given theorems, in a given proof system.
  • Be able to express and formalize in a logical language useful properties of models such as transition systems, and be able to determine the truth or falsity of such formulas in a given model.

Synopsis

Approximately 16 lectures.

Propositional logic (7 Lectures).

  1. Introduction. Syntax of propositional logic. Examples. Recursive definitions of functions over formulas.
  2. Semantics of propositional logic. Validity and satisfiability of formulas. Truth tables. Modern SAT-solving.
  3. Equivalence of formulas. Substitution. Normal forms.
  4. Resolution.
  5. Sequent calculus.
  6. Sequent calculus (ctd.). Soundness and completeness.

First-order logic (6 Lectures).

  1. Structures and examples for structures. Sub-structures.
  2. Introduction. Syntax of first-order logic. Examples.
  3. Semantics.
  4. Examples. Satifiability and validity. Evaluation of formulas.
  5. Sequent Calculus.
  6. Sequent Calculus (ctd.). Examples. Soundsness and completeness.

Linear Temporal Logic [LTL] (3 lectures).

  1. Introduction. Syntax of LTL. Examples.
  2. Semantics of LTL.
  3. Model checking LTL formulas.

 

Syllabus

Syntax and Semantics of propositional and first-order logic. Proofs by induction on the structure of formulas. Formal proofs using sequent calculus. Resolution. Brief discussion of issues of soundness and completeness. Mathematical models of computation, especially Kripke structures. Temporal logics: Linear Temporal Logic (LTL). Determining the truth of a temporal logic formula in a given model.

Reading list

Primary text:
  • Mathematical logic, 2nd edition, by H.-D. Ebbinghaus, J. Flum and W. Thomas (Springer 1996).
  • Logic in computer science: modelling and reasoning about systems,2nd edition, by M. Huth and M. Ryan (Cambridge University Press, Cambridge 2004).
Other texts to be consulted
  • Proof and Disproof in Formal Logic, by Richard Bornat (Oxford University Press, 2005).
  • Logic for Computer Science, by S. Reeves and M. Clarke (International Computer Science Series, OMW, University of London, Addison-Wesley, 1990).
  • The language of first-order logic: including the Mackintosh version of Tarski's World 4.0, by J. Barwise and J. Etchemendy (CSLI Lecture Notes no. 23, CSLI Publications, Stanford 1993).
  • Hyperproof by J. Barwise and J. Etchemendy (CSLI Lecture Notes no. 42, CSLI Publications, Stanford 1994).

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.