COM2107 Logic in Computer Science
| Summary |
This module introduces the foundations of logic in computer science. The first part introduces the syntax and semantics of propositional and
predicate logics, natural deduction, and notions such as soundness, completeness and (un)decidability. The second part covers applications in
computer science and beyond, such as automated reasoning and decision procedures, modal and temporal logics for the verification of computing
systems, and type systems for programming languages. |
| Session |
Spring 2025/26 |
| Credits |
10 |
| Assessment |
- Formal Examination
- Knowledge quizzes
|
| Lecturer(s) |
Dr Jonni Virtema |
| Resources |
|
| Aims |
This unit aims to:
- Introduce the standard logics in computer science and their associated proof systems and the main applications of logic in computer
science;
- Enhance analytical and logical skills in reasoning abstractly (about computation and computational modelling);
- Provide a thorough grounding for theoretical courses at more advanced levels.
|
| Learning Outcomes |
By the end of the unit, a candidate will be able to:
- Be able to perform proofs in propositional, predicate and modal logics (aims 1 and 2);
- Explain the principles of automated theorem provers, such as the DPLL and the resolution method (aims 1 and 2);
- Be able to apply formal languages and reasoning to the design and verification of computing systems (aims 1 to 3).
|
| Content |
- syntax and semantics of propositional and predicate logic
- natural deduction systems for these logics
- applications of logic in computing and systems engineering (e.g. automated and interactive theorem proving, basics of model checking, types in programming)
|
| Teaching Method |
- 2 formal lectures plus 1 exercise/tutorial session per week.
|
| Feedback |
Weekly feedback is provided in the exercise/tutorial sessions. |
|
