# Logic and Proof:  2008-2009

 Lecturer Stephan Kreutzer 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).

1. Introduction. Syntax of propositional logic. Examples.
2. Truth tables. Modern SAT-solving.
3. Natural deduction.
4. Natural deduction (ctd.). Soundness and completeness.

First-order logic (5 Lectures).

1. Introduction. Syntax of first-order logic. Examples.
2. Semantics.
3. Natural deduction.
4. Natural deduction.
5. Soundness and completeness; incompleteness.

Models of computation (1 lecture).

1. Kripke structures and brief mention of other models.

Linear Temporal Logic [LTL] (3 lectures).

1. Introduction. Syntax of LTL. Examples.
2. Semantics of LTL.
3. Model checking LTL formulas.

Computation Tree Logic [CTL] (3 lectures).

1. Introduction. Syntax of CTL. Examples.
2. Semantics of CTL.
3. 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.