0.1: Course Overview
This course is based on the following philosophical principle:
All computing scientists must be able to employ rigorous reasoning
to justify their claims about the behaviour of the programs they produce.
Thus the goal of this course is to introduce you to the logical and
mathematical tools for reasoning about algorithms.
Being able to effectively use these tools makes the difference between
being a programming hack and a computing scientist.
However, a course such as this can only examine the elementary material.
We will be covering in depth a small number of essential ideas.
The course contains three main parts:
- Reasoning about programs.
Throughout the course we will be looking at programs
as formal objects.
Our goal will be to precisely specify the behaviour we wish our programs
to have, and then to develop programs and prove that they have the
desired behaviour.
- A formal system for predicate logic.
In this part we will introduce and use a formal system for predicate
logic.
Unlike previous versions of this course, and many courses on logic, we
will not be using a system that exists only on paper.
Instead we will be writing proofs that can be checked for
correctness using the Mizar MSE system.
In much the same way that you write a program, you will be entering
your proofs into files and running them through Mizar.
By the end of this part of the course you should be very comfortable
with the idea of a proof, how to read one, and to some extent,
how to write one.
- Basics: Sets, Relations, Functions, and Induction. This could have
been the first part of the course.
We will introduce as required, various concepts
such as sets, relations, functions, types, induction, and basic number
theory.
NOTE: Parts 1 and 3 above are not included in this document. -- FL