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).