Logic and Proof

Overview

The main aim of the course is to give a first introduction to formal logic for computer scientists. There are four main parts to the course.

Brief Introduction to some finite models for computation. Finite Graphs. Finite Databases. Finite Transition Systems. Examples.

Introduction to First-order logic. Syntax of first-order logic. Semantic explanation of first-order logic (i.e. truth values, models) illustrated by finite "meaningful" examples, in the style of Barwise and Etchemenedy's "Tarski's World". Examples such as specifying blocks-world scenarios, databases - and finite transition systems, as motivated by Part 1.

Introduction to Formal Proof. Building on Part 2, the question of formal inference in first-order logic is addressed. Natural deduction rules are presented. The issues of soundness and completeness are raised. The issue of decidability is informally explained.

Brief introduction to alternative logical formalisms . Fragments of first-order logic which are computationally tractable and interesting in applications: modal logic, equational logic. (Brief mentioning:) finite-variable logics, the logic of iteration (Kleene-star modality). Alternative presentations: game semantics for first-order logic; (optional, if time permits:) semantic tableaux.

Learning Outcomes

At the end of the course students are expected to:

• Be able to give some basic examples of (finite) mathematical structures used in CS.
• Understand and be able to explain and illustrate the meaning of given logical formulas, using such mathematical models.
• Be able to express and formalize in a logical language useful properties of the models.
• Perform model checking for given formulas over a given model.
• Construct simple, but rigorous, formal proofs for some given theorems, in a given proof system.