Single-Course Engelsk 5 ECTS

Automated Reasoning

DTU Compute

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.

See course description in Danish

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

Jørgen Villadsen

Contact or read more about Jørgen
Jørgen Villadsen

See course in the course database.

Registration

Language

Engelsk
Duration

13 weeks
Institute

Compute
Place

DTU Lyngby Campus
Course code 02256
Course type Candidate
Semester start Week 6
Semester end Week 20
Days Thurs 13-17
Price

9.250,00 DKK

Related educations

Registration