**All computing scientists must be able to employ rigorous reasoning to justifytheir claims about thebehaviorof the programs they produce.**

**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

**Introduction to Logic in Computing Science**

**University of Alberta - Department of Computing Science**

**CMPUT 172**