Logic and Proof: 2012-2013
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.
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.
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.
- Polynomial-time algorithms for Horn formulas and 2-SAT.
- Resolution: soundness and refutation completeness.
- The Davis-Putnam procedure.
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.
- 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.
- Introduction to propositional logic. Syntax of propositional logic. Truth tables. Resolution. Davis-Putnam procedure. Notions of soundness and completeness.
- 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. Unification and resolution for predicate logic.
- Decidable theories.
- Introduction to Linear Temporal Logic. Kripke structures and model checking.
- Logic for Computer Scientists. Uwe Schoning. Modern Birkäuser Classics, Reprint of the 1989 edition.
- Logic in computer science: modelling and reasoning about systems,2nd edition, by M. Huth and M. Ryan (Cambridge University Press, Cambridge 2004).