Introduction to Formal Reasoning
| Code | School | Level | Credits | Semesters |
| COMP2068 | School of Computer Science | 2 | 10 | Autumn China |
- Code
- COMP2068
- School
- School of Computer Science
- Level
- 2
- Credits
- 10
- Semesters
- Autumn China
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
Only available for Level 2 computer science & computer science with AI students
Classes
- One 1-hour tutorial each week for 11 weeks
- Two 1-hour lectures each week for 11 weeks
- One 1-hour computing each week for 11 weeks
Assessment
- 25% Coursework 1: Coding exercise
- 75% Exam 1 (2-hour)
Assessed by end of autumn semester
Educational Aims
The aim of this module is to develop mathematical and formal reasoning skills necessary to specify and reason about programs and/or mathematical problems.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.