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 2021/22 
Credits 
10 
Assessment 

Lecturer(s) 
Dr Mike Stannett & 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.

Objectives 
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. 
Recommended Reading 
Course lecture notes and the literature mentioned in these.
