NDAB16011U Logic in Computer Science (LICS)
BSc Programme in Computer Science
The aim of this course is to provide a firm theoretical
foundation of formal logic, with an emphasis on logics, properties,
techniques and algorithms relevant in computer science. Building on
the students' existing knowledge of Boolean logic and
mathematical reasoning, the course includes both fundamental logic
formalisms and more specialized logics used in modelling,
specification, and verification of programs and hardware systems.
The course covers introductions to
- propositional logic,
- predicate logic,
- temporal logics LTL and CTL,
- model checking,
- binary decision diagrams, and
- formalised proving using a proof assistant.
At course completion, the successful student will have
- Defining logics in terms of syntax, semantics and natural deduction systems, and formal reasoning about logical formulas.
- A selection of specific logics, including propositional logic, predicate logic and temporal logic (e.g. LTL and CTL).
- Fundamental properties of these logics, such as soundness, completeness and decidability.
- Algorithms for transforming logical formulas to normal forms; for deciding fundamental properties of logical formulas such as satisfiability, validity, and entailment; and (symbolic) model checking by binary decision diagrams (BDDs).
- Deciding and proving formal properties of logical formulas (e.g. satisfiability, validity, implication and equivalence) both by semantics and natural deduction arguments.
- Proving properties relating logical inference systems and semantics, specifically soundness or completeness.
- Applying specific algorithms for deciding properties of logical formulas: SAT solvers for propositional calculus; model checking LTL/CTL; using BDDs to represent Boolean functions and perform symbolic model checking.
- Performing any of the above in the context of variants of the presented logics.
- Use formal logic to describe real-world situations, express properties of programs and reason about them formally.
- Expected to be "Logic in Computer Science", 2nd Edition; by Michael Huth and Mark Ryan, Cambridge University Press, 2004, ISBN 0-521-54310X.
- Supplementary notes.
Problem solving and programming (PoP) or equivalent: Functions, recursion, lists, user-defined data types.
obligatory written exercises.
- 7,5 ECTS
- Type of assessment
- Written examination, 4 hours under invigilationWritten 4-hour exam with invigilation.
- Exam registration requirements
There will be 6 weekly homework sets during the course: at least 5 of the 6 sets must be completed satisfactorily to qualify for taking the exam. Unsatisfactorily or partially satisfactorily homework solutions can be resubmitted once except for the last homework set, where no resubmission is possible.
- Written aids allowed
- Marking scale
- 7-point grading scale
- Censorship form
- No external censorship
Multiple internal examiners.
Same format as for the ordinary exam. Qualification requires 5 satisfactory homework solutions, including previous solutions already turned in prior to the ordinary exam. These must be handed in no later than 2 weeks before the re-exam.
If less than 10 students are signed up for the re-exam, the re-exam will be an oral exam (30 minutes including grading) after preparation (60 minutes) with written aids only (no electronic aids).
Criteria for exam assesment
See Learning Outcome.
- Theory exercises