Logic II, 6.0 credits

Logik II, 6.0 hp

6FIDA16

Course level

Third-cycle Education

Description

We introduce participants to a broad scope on modern logics and their applications in computer science. In particular, we consider aspects that are relevant for artificial intelligence, automated theorem proving, formal specifications, and software verification.

We discuss aspects on incomplete and inaccurate information. Due to the broad nature of the course we primarily provide foundational aspects and enable participants to selfstudy by suggesting concepts and an entry points to the literature.

Contact

Entry requirements

Doctoral students with foundational background in logics (e.g. introductory course).

Learning outcomes

After successful completion of the course, students are able to:

  • assess proofs by proof assistants and/or validity techniques
  • chose and/or develop a logic for a particular application domain
  • assess limitations in logics and employ these to draw conclusions
  • execute and understand the presented methods and concepts for non-classical logics
  • apply logics for one of the following topics automated solving, verification, or causal reasoning

Contents

  • Proof and model theory
  • Extensions/restrictions of classical logics, e.g, second-order logic
  • Basic introduction to non-classical logics: three-valued logics, modal logic, description logic
  • Depending on the background of the group
    • Applications to computational complexity: MSO, TQBF
    • Answer Set Programming, Certified Reasoning/Verification, or Causal Reasoning

We introduce participants to a broad scope on modern logics and their applications in computer science. In particular, we consider aspects that are relevant for artificial intelligence, automated theorem proving, formal specifications, and software verification.

We discuss aspects on incomplete and inaccurate information. Due to the broad nature of the course we primarily provide foundational aspects and enable participants to selfstudy by suggesting concepts and an entry points to the literature.

Educational methods

Organization

- Course will be held in presence/via Zoom.

- Course is offered in a blocked format, dates will be agreed on in the first sessions

- The course is given in an intensive format ("crash course”).

- Expect a mix between lectures, classes, and group presentations/discussions of assignments

- Course material will be in English

Examination

  • 50% Group assignment on a topic of your choice, where you read and summarize two-three research papers and put them in context of the learnt material
    • OR apply learnt knowledge to a practical encoding
    • OR theoretically improve existing techniques
  • 50% Individual take home exam

Grading

Two-grade scale

Course literature

Provided in the lecture notes .

General information

Interest registration: Contact Anne Moe, anne.moe@liu.se