Logic in Computer Science

Powerful tools for verifying software and hardware systems have been developed. These tools rely in a crucial way on logical techniques. This course provides a sound basis in logic and a short introduction to some logical frameworks used in modelling, specifying and verifying computer systems. A sound basic knowledge in logic is a welcome prerequisite for courses in program verification, formal methods and artificial intelligence. The course covers propositional and predicate calculus, and model-checking. More concretely, the course gives a thorough introduction to fundamental notions of logic such as natural deduction, semantics of both propositional and predicate calculus, soundness and completeness, conjunctive normal forms, Horn clauses, undecidability and expressiveness of predicate logic, plus an introduction to model checking: Linear-time temporal logic (LTL) and Branching-time temporal logic (CTL). Sub-courses<br> **1\. Written hall examination** (Skriftlig salstentamen), 7.5 credits<br> Grading scale: Pass with distinction (5), Pass with credit (4), Pass (3) and Fail (U)