Introduction to Formal Reasoning

Code

COMP2065

School

Computer Science

Level

2

Credits

10

Semesters

Autumn UK

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. This module is part of the Foundations of Computer Science theme in the School of Computer Science.

Classes

Tutorials and Computing will not necessarily occur in every week.

Assessment

• 25% Coursework 1: Lab-based coursework. Reassessment for the module is 100% ExamSys (in person) exam.
• 25% In-class test 1: Lab-based test. Reassessment for the module is 100% ExamSys (in person) exam.
• 50% Exam 1 (2-hour): Written exam. Reassessment for the module is 100% Written (in person) exam.

Assessed by end of autumn 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

• Professor Thorsten Altenkirch