![Scenic walk through Manchester centre on industrial placement](http://contentlibrary.manchester.ac.uk/_coursemarketing/UMANC/2024/9/00490/U_8_(2).jpg)
- UCAS course code
- GG41
- UCAS institution code
- M20
BSc Computer Science and Mathematics with Industrial Experience
Year of entry: 2024
- View tabs
- View full page
Course unit details:
Logic and Modelling
Unit code | COMP21111 |
---|---|
Credit rating | 10 |
Unit level | Level 2 |
Teaching period(s) | Semester 1 |
Available as a free choice unit? | Yes |
Overview
Pre/co-requisites
Unit title | Unit code | Requirement type | Description |
---|---|---|---|
Mathematical Techniques for Computer Science | COMP11120 | Pre-Requisite | Compulsory |
Linear Algebra | MATH11022 | Pre-Requisite | Compulsory |
Mathematical Foundations & Analysis | MATH11121 | Pre-Requisite | Compulsory |
Pre-requisites
To enrol students are required to have taken COMP11120 or one of the following: MATH10111, MATH10131 , MATH10212, MATH10232.
Aims
This course intends to build an understanding of fundamentals of (mathematical) logic as well as some of the applications of logic in modern computer science, including hardware verification, finite domain constraint satisfaction and verification of concurrent systems.
Learning outcomes
-
Have a knowledge about basic reasoning (or satisfiability-checking) algorithms for propositional logic.
-
Have a knowledge of quantified boolean formulas and basic understanding of bound variables and quantifiers.
-
To understand BDDS (binary decision diagrams) as a data structure for compact representation of propositional formulas.
-
Have a knowledge about applications of propositional logic (such as finite domain constraint satisfaction and planning) and be able to apply it for solving hard combinatorial problems.
-
Have a knowledge of simple temporal logics.
-
Be able to formally specify finite-state concurrent systems as transition systems.
-
Be able to specify properties of simple transition systems in temporal logics.
Syllabus
- Propositional logic
- Conjunctive normal form (CNF)
- DPLL satisfiability algorithm
- Randomized satisfiability algorithms
- Compact representations of Boolean functions using BDTs/BDDs/OBDDs
- Quantified Boolean Logic (QBF) Splitting and DPLL algorithms for QBF
- Propositional logic of finite domains
- State-changing systems
- Linear temporal logic (LTL)
- Model checking
Teaching and learning methods
Lectures
22 in total, 2 per week, including some feedback sessions on exercises
Employability skills
- Analytical skills
- Innovation/creativity
- Problem solving
- Research
Assessment methods
Method | Weight |
---|---|
Written exam | 50% |
Written assignment (inc essay) | 50% |
Feedback methods
Recommended reading
COMP21111 reading list can be found on the Department of Computer Science website for current students.
Study hours
Scheduled activity hours | |
---|---|
Assessment written exam | 2 |
Lectures | 24 |
Practical classes & workshops | 9 |
Independent study hours | |
---|---|
Independent study | 65 |
Teaching staff
Staff member | Role |
---|---|
Konstantin Korovin | Unit coordinator |
Additional notes
Course unit materials
Links to course unit teaching materials can be found on the School of Computer Science website for current students.