Introduction to Formal Reasoning

Code

COMP2067

School

Computer Science

Level

2

Credits

10

Semesters

Spring Malaysia

Summary

This module is an introduction to formal reasoning with applications in program verification and Mathematics. We will use an interactive proof system like Lean or Coq to learn how to make precise statements and how to verify them using formal proofs. At the same time we develop skills in informal reasoning. Topic covered are: propositional logic, classical principles, predicate logic, the theories of Booleans, natural numbers, lists and trees. Verification of simple algorithms.

Target Students

Available to Level 2 undergraduate students in the School of Computer Science. Available to inter-campus mobility students and other exchange students in Computer Science. This module is part of the Foundations of Computer Science theme in the School of Computer Science.

Classes

• One 1-hour tutorial each week for 12 weeks
• One 2-hour lecture each week for 12 weeks
• One 1-hour computing each week for 12 weeks

Assessment

• 25% Coursework 1: Coursework
• 75% Exam 1 (2-hour): 2-hour written examination. Reassessment is 100% exam.

Assessed by end of spring semester

Educational Aims

Learning Outcomes

Knowledge and Understanding

To understand logical reasoning and proofs and their application in computer science.

Intellectual Skills

The ability to understand and apply simple logical reasoning. To be able to understand the specification of data structures and algorithms.

Professional Skills

To be able to use formal reasoning tools to verify the correctness of software systems.

Transferable Skills

To understand how to specify a problem precisely and how to give evidence for a statement.
The ability to use mathematics to solve problems.

Conveners

• Kweh Yeah Lun