Skip to navigation | Skip to main content | Skip to footer
Menu
Menu

COMP21111 Logic and Modelling syllabus 2019-2020

COMP21111 materials

COMP21111 Logic and Modelling

Level 2
Credits: 10
Enrolled students: 101

Course leader: Konstantin Korovin


Additional staff: view all staff

Requisites

  • Pre-Requisite (Compulsory): COMP11120
  • Pre-Requisite (Compulsory): MATH10111
  • Pre-Requisite (Compulsory): MATH10131
  • Pre-Requisite (Compulsory): MATH10212
  • Pre-Requisite (Compulsory): MATH10232

Additional requirements

  • 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.

Assessment methods

  • 80% Written exam
  • 20% Coursework
Timetable
SemesterEventLocationDayTimeGroup
Sem 1 Lecture Schuster BRAGG TH Thu 16:00 - 18:00 -
Sem 1 w3+ Examples G41 Fri 15:00 - 16:00 F
Sem 1 w3+ Examples G41 Fri 16:00 - 17:00 G
Themes to which this unit belongs
  • Rigorous Development

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

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.

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 methods

Lectures

22 in total, 2 per week, including some feedback sessions on exercises

Feedback methods

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

Study hours

  • Assessment written exam (2 hours)
  • Lectures (24 hours)
  • Practical classes & workshops (9 hours)

Employability skills

  • Analytical skills
  • Innovation/creativity
  • Problem solving
  • Research

Learning outcomes

On successful completion of this unit, a student will be able to:

  • 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.

Reading list

COMP21111 does not have a specified reading list.

Additional notes

Course unit materials

Links to course unit teaching materials can be found on the School of Computer Science website for current students.