Logic and Proof

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.