Logic and Proof: 20122013
Lecturer 

Degrees 

Term 
Hilary Term 2013 (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 SATsolving, model checking and automated theorem proving.
The course relates to a number of thirdyear and fourthyear options. Temporal logic is used extensively in ComputerAided 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 viceversa.
 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.
 Compactness Тheorem.
 Polynomialtime algorithms for Horn formulas and 2SAT.
 Resolution: soundness and refutation completeness.
 The DavisPutnam procedure.
Firstorder 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.
 Unification and resolution for predicate logic.
 Decidable theories.
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. DavisPutnam procedure. Notions of soundness and completeness.
 Introduction to firstorder logic. Syntax of firstorder logic. Semantics of firstorder logic: graphs, strings, databases and number systems as firstorder structures.
 Prenex form and Skolemisation.
 Herbrand models and ground resolution. Unification and resolution for predicate logic.
 Decidable theories.
 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).