This course is based on the following philosophical principle:
- All computing scientists must be able to employ rigorous reasoning to justifytheir claims about thebehaviorof the programs they produce.
Thus the goal of this course is to introduce you to the logical and mathematical tools forreasoning about algorithms. Being able to e?ectively use these tools makes the di?erencebetween being a programming hack and a computing scientist. However, a course such asthis can only examine the elementary material.
kinlane-productions2
The course containsthree 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 ?les 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 ?rst part of the course. We will introduce as required, various concepts such as sets, relations, functions, types, induction, and basic number theory
Tweedledee (to Alice): I know what you are thinking about, but it isn't so, nohow.
Tweedledum: Contrariwise, if it was so, it might be; if it were so, it would be; but as it isn't, it ain't.
That's logic.
Introduction to Logic in Computing Science
University of Alberta - Department of Computing Science
CMPUT 172
