BSc Computer Science and Mathematics / Course details
Year of entry: 2022
- View tabs
- View full page
Course unit details:
Logic and Modelling
|Unit level||Level 2|
|Teaching period(s)||Semester 1|
|Offered by||Department of Computer Science|
|Available as a free choice unit?||Yes|
|Unit title||Unit code||Requirement type||Description|
|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|
|Mathematical Techniques for Computer Science||COMP11120||Pre-Requisite||Compulsory|
To enrol students are required to have taken COMP11120 or one of the following: MATH10111, MATH10131 , MATH10212, MATH10232.
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.
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.
- 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
22 in total, 2 per week, including some feedback sessions on exercises
- Analytical skills
- Problem solving
|Written assignment (inc essay)||50%|
COMP21111 reading list can be found on the Department of Computer Science website for current students.
|Scheduled activity hours|
|Assessment written exam||2|
|Practical classes & workshops||9|
|Independent study hours|
|Konstantin Korovin||Unit coordinator|
Course unit materials
Links to course unit teaching materials can be found on the School of Computer Science website for current students.