Single-Course English 5 ECTS

Automated Reasoning

Overall Course Objectives

Reasoning is the ability to make logical inferences. The aim of the course is to give the students an introduction to automatic and interactive computer systems for reasoning about mathematical theorems as well as properties of IT systems. It will cover theoretical insight as well as practical skills in relevant proof assistants.

Learning Objectives

  • explain the basic concepts introduced in the course
  • express mathematical theorems and properties of IT systems formally
  • master the natural deduction proof system
  • relate first-order logic, higher-order logic and type theory
  • construct formal proofs in the procedural style and in the declarative style
  • use automatic and interactive computer systems for automated reasoning
  • evaluate the trustworthiness of proof assistants and related tools
  • communicate solutions to problems in a clear and precise manner

Course Content

The natural deduction proof system, first-order logic, higher-order logic and type theory. Formal proofs in the procedural style and in the declarative style using automatic and interactive provers. The Isabelle proof assistant in artificial intelligence and computer science.

Recommended prerequisites

02156/02157/02180, Proof systems for first-order logic, functional programming, basic algorithms in artificial intelligence. Mathematical maturity. Logic programming is an advantage.

Teaching Method

Lectures, exercises and mandatory assignments.

Faculty

See course in the course database.

Registration

Language

English

Duration

13 weeks

Institute

Compute

Place

DTU Lyngby Campus

Course code 02256
Course type Candidate
Semester start Week 5
Semester end Week 19
Days Thurs 13-17
Price

7.500,00 kr.

Registration