Kursussøgning, efter- og videreuddannelse – Københavns Universitet

Videresend til en ven Resize Print Bookmark and Share

Kursussøgning, efter- og videreuddannelse

Logic in Computer Science (LICS)

Practical information
Study year 2016/2017
Time
Block 1
Programme level Bachelor
ECTS 7,5 ECTS
Course responsible
  • Fritz Henglein (8-7b78817a7f787c8153777c417e8841777e)
  • Department of Computer Science
Course number: NDAB16011U

Course content

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,
  • the temporal logics LTL and CTL,
  • model checking,
  • binary decision diagrams, and
  • formalised proving using a proof assistant.

 

Learning outcome

At course completion, the successful student will have

Knowledge of:

  • 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).


Skills in:

  • 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.


Competences to:

  • Use formal logic to describe real-world situations and express properties of programs, and reason about them formally.

 

Recommended prerequisites

Discrete mathematical structures (DiMS) or Discrete mathematics and algorithms (DMA) or Discrete mathematics (DIS) or Discrete mathematics for first-year students (DisRus) or other course(s) covering basic arithmetic, sets, relations, functions, big-O-notation, graphs and basic, proofs by induction, mathematical reasoning by deductive arguments.

Problem solving and programming (PoP) or equivalent: Functions, recursion, lists, user-defined data types.

Sign up


As an exchange, guest and credit student - click here!

Continuing Education - click here!

Education

BSc Programme in Computer Science
 

Studyboard

Study Board of Mathematics and Computer Science

Course type

Single subject courses (day)

Duration

1 block

Schedulegroup

C
---- SKEMA LINK ----

Teaching and learning methods

2 lectures of 2 hours each and 1 exercise/discussion session of 4 hours per week;
obligatory written exercises.

Capacity

No limit.

Language

English

Literature

  • 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.

Workload

Category Hours
Lectures 28
Exam 17
Theory exercises 14
Preparation 147
English 206

Exam

Type of assessment

Written examination, 4 hours under invigilation
Written 4-hour exam with invigilation.

The course has been selected for ITX exam at Peter Bangs Vej.

Aid

Written aids allowed

Marking scale

7-point grading scale

Criteria for exam assessment

See "Learning Outcome."

Censorship form

No external censorship
Multiple internal examiners.

Re-exam

Same exam format as for reexam.  Qualification requires 5 satisfactory homework solutions, including previous solutions already turned in prior to regular exam, if any. 

If at most 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).

Mere information om kurset
Er du BA- eller KA-studerende?
Er du bachelor- eller kandidat-studerende, så find dette kursus i kursusbasen for studerende:

Kursusinformation for indskrevne studerende