Don't just imagine your future at University, experience it first-hand!

Step into the shoes of an undergraduate student and join us for our upcoming on-campus Discover Days in Science, Engineering and Fashion. These days are tailored exclusively for Year 12s who are interested in taking their academic journey to the next level. Find your favourite subject now!

# BSc Computer Science and Mathematics with Industrial Experience

Year of entry: 2024

## Course unit details:Logic and Modelling

Unit code COMP21111 10 Level 2 Semester 1 Yes

### Overview

This is a unique course developed at the University of Manchester. It explains how implementations of logic can be used to solve a number a number of problems, such as solving hardest Sudoku puzzles in no time, analysing two-player games, or finding serious errors in computer systems

### Pre/co-requisites

Unit title Unit code Requirement type Description
Mathematical Techniques for Computer Science COMP11120 Pre-Requisite Compulsory
Mathematical Foundation & Analysis MATH11121 Pre-Requisite Compulsory
Foundations of Pure Mathematics B MATH10111 Pre-Requisite Compulsory
Calculus and Vectors B MATH10131 Pre-Requisite Compulsory
Linear Algebra B MATH10212 Pre-Requisite Compulsory
Calculus and Applications B MATH10232 Pre-Requisite Compulsory
Students who are not from the School of Computer Science must have permission from both Computer Science and their home School to enrol.

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

My Website of this course will contain a lot of material, including solutions to exercises

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