The University of Sheffield
Department of Computer Science

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 2021/22
Credits 10
Assessment
  • Formal Examination
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.