Logic and Proof: 2011-2012
Information
|
Lecturer |
|
|
Degrees |
|
|
Term |
Hilary Term 2012 (16 lectures) |
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).
- Syntax of propositional logic. Translating combinatorial problems to propositional logic. Truth tables.
- Validity and satisfiability of formulas. Logical equivalence and algebraic reasoning.
- Normal forms: CNF, DNF, Tseitin's encoding.
- Polynomial-time algorithms for Horn formulas and 2-SAT.
- Resolution: soundness and refutation completeness.
- Compactness Theorem.
First-order logic (7 Lectures).
- Signatures, structures and valuations.
- Examples: graphs, trees, strings, relational databases and number systems.
- Formula evaluation on finite structures.
- Prenex normal form and Skolemisation.
- Herbrand models and ground resolution.
Temporal Logic (2 lectures).
- Linear Temporal Logic (LTL) and example specifications.
- Semantics of LTL, including basic equivalences
- Model checking LTL formulas by inspection.
Syllabus
- Introduction to propositional logic. Syntax of propositional logic. Truth tables. Resolution. Notions of soundness and completeness. Proofs by induction on the structure of formulas.
- 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.
- 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).