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

1. Syntax of propositional logic.  Translating combinatorial problems to propositional logic.  Truth tables.
2. Validity and satisfiability of formulas.  Logical equivalence and algebraic reasoning.
3. Normal forms: CNF, DNF, Tseitin's encoding.
4. Polynomial-time algorithms for Horn formulas and 2-SAT.
5. Resolution: soundness and refutation completeness.
6. Compactness Theorem.

First-order logic (7 Lectures).

1. Signatures, structures and valuations.
2. Examples: graphs, trees, strings, relational databases and number systems.
3. Formula evaluation on finite structures.
4. Prenex normal form and Skolemisation.
5. Herbrand models and ground resolution.

Temporal Logic (2 lectures).

1. Linear Temporal Logic (LTL) and example specifications.
2. Semantics of LTL, including basic equivalences
3. 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.