Logic in Computer Science (LICS)

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


Note that while some applications of logic will be covered in some detail during the course, the focus of the course is primarily on the theoretical foundations of logic in computer science rather than its concrete applications.

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, express properties of programs and reason about them formally.

 

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

The syllabus will be posted in Absalon.

In previous years the syllabus has included:

  • "Logic in Computer Science"; by Michael Huth and Mark Ryan. Latest edition.
  • Supplementary notes.

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

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

Written
Individual
Continuous feedback during the course of the semester
ECTS
7,5 ECTS
Type of assessment
On-site written exam, 4 hours under invigilation
Type of assessment details
The on-site written exam is an ITX exam.
See important information about ITX-exams at Study Information, menu point: Exams -> Exam types and rules -> Written on-site exams (ITX)
Exam registration requirements

There will be 6 weekly assignments during the course, graded on a scale from 0 to 2 points: at least 10 points are required to be qualified for the exam.

Unsatisfactorily or partially satisfactorily assignments can be resubmitted once except for the last assignment, where no resubmission is possible.

Aid
Written aids allowed

 

Books, notes, and similar materials can be brought in paper form or uploaded before the exam and accessed digitally from the ITX computer. Read more about this at Study Information.

Marking scale
7-point grading scale
Censorship form
No external censorship
Several internal examiners
Re-exam

Same as ordinary exam. 

Qualification for the re-exam requires 10 points or more from assignments, including previous solutions already handed in prior to the ordinary exam. These must be handed in no later than 3 weeks before the re-exam week.

If less than 10 students register for the re-exam, the re-exam will be a 30 minutes oral exam (including grading) after preparation (60 minutes) with written aids only (no electronic aids).

Criteria for exam assessment

See Learning Outcome.

Single subject courses (day)

  • Category
  • Hours
  • Lectures
  • 28
  • Preparation
  • 146
  • Theory exercises
  • 28
  • Exam
  • 4
  • English
  • 206

Kursusinformation

Language
English
Course number
NDAB16011U
ECTS
7,5 ECTS
Programme level
Bachelor
Duration

1 block

Placement
Block 2
Schedulegroup
A
Capacity
No limitation – unless you register in the late-registration period (BSc and MSc) or as a credit or single subject student.
Studyboard
Study Board of Mathematics and Computer Science
Contracting department
  • Department of Computer Science
Contracting faculty
  • Faculty of Science
Course Coordinator
  • Robert Glück   (6-6a6f7868666e43676c316e7831676e)
Saved on the 07-05-2024

Are you BA- or KA-student?

Are you bachelor- or kandidat-student, then find the course in the course catalog for students:

Courseinformation of students