Logic and Proof: 2008-2009
Lecturer | |
Degrees | |
Term | Hilary Term 2009 (16 lectures) |
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. Natural deduction. Notions of soundness and completeness.
- Introduction to first-order logic. Syntax of first-order logic. Semantics of first-order logic. Examples. Natural deduction. Notions of soundness and completeness, and brief discussion of incompleteness and undecidability.
- Introduction to some finite models for computation, in particular Kripke structures. Examples.
- Introduction to temporal logics, especially Linear Temporal Logic (LTL) and Computation Tree Logic (CTL).
- Time permitting: discussion of model-checking algorithms.
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 Kripke structures, and be able to determine the truth or falsity of such formulas in a given model.
Synopsis
Approximately 16 lectures.
Propositional logic (4 Lectures).
- Introduction. Syntax of propositional logic. Examples.
- Truth tables. Modern SAT-solving.
- Natural deduction.
- Natural deduction (ctd.). Soundness and completeness.
First-order logic (5 Lectures).
- Introduction. Syntax of first-order logic. Examples.
- Semantics.
- Natural deduction.
- Natural deduction.
- Soundness and completeness; incompleteness.
Models of computation (1 lecture).
- Kripke structures and brief mention of other models.
Linear Temporal Logic [LTL] (3 lectures).
- Introduction. Syntax of LTL. Examples.
- Semantics of LTL.
- Model checking LTL formulas.
Computation Tree Logic [CTL] (3 lectures).
- Introduction. Syntax of CTL. Examples.
- Semantics of CTL.
- Model checking CTL formulas
Syllabus
Syntax and Semantics of propositional and first-order logic. Formal proofs using natural deduction. Brief discussion of issues of soundness, completeness, and incompleteness. Mathematical models of computation, especially Kripke structures. Temporal logics: Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). Determining the truth of a temporal logic formula in a given model.Reading list
Primary text:- Logic in computer science: modelling and reasoning about systems,2nd Editions, by M. Huth and M. Ryan (Cambridge University Press, Cambridge 2004).
- 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).
- Mathematical Logic by H.D. Ebbinghaus, J. Flum, W. Thomas (Undergraduate Texts in Mathematics, Springer Verlag 1984).
- 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).
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.