Arvutiteaduse instituut
  1. Kursused
  2. 2022/23 sügis
  3. Interaktiivne teoreemide tõestamine (LTAT.04.014)
EN
Logi sisse

Interaktiivne teoreemide tõestamine 2022/23 sügis

  • HomePage

Intro

When humans prove the correctness of mathematical theorems, they naturally make mistakes. Subtle mistakes can stay unnoticed for a long time, while other works build on incorrect theorems. Every person who wants to make sure that a result is correct needs to check the whole proof in detail, leading to a huge duplication of effort.

(Computer-aided) theorem proving seeks to alleviate those issues. Once the computer has verified a proof, we do not manually verify it over and over, and we do not need to rely on humans not making mistakes.

There are roughly speaking two kinds of theorem proving: automated theorem proving where the computer fully automatically proves the theorem (or fails), and interactive theorem proving where a human guides the computer through the proof until the computer is satisfied.

This course aims to introduce the latter:

  • How to use an interactive theorem prover (using Isabelle/HOL as the working example)
  • How an interactive theorem prover works

The course consists of two parts:

  • The first half of the semester, we introduce the interactive theorem proving using Isabelle/HOL. (Lectures and homeworks and practice sessions.)
  • The second half is project group work, working on individual topics. Those topics can either be proving some interesting theorem in Isabelle/HOL, or implementing some small theorem proving related project. Lectures will continue with the goal of supporting the projects.

Lecture data

  • Lecturer: Dominique Unruh
  • Lecture: Mondays, 14:15–15:45. Δ-2045
  • Practice: Wednesdays, 10:15–11:45. Δ-2010
  • Volume: 6 ECTS
  • Arvutiteaduse instituut
  • Loodus- ja täppisteaduste valdkond
  • Tartu Ülikool
Tehniliste probleemide või küsimuste korral kirjuta:

Kursuse sisu ja korralduslike küsimustega pöörduge kursuse korraldajate poole.
Õppematerjalide varalised autoriõigused kuuluvad Tartu Ülikoolile. Õppematerjalide kasutamine on lubatud autoriõiguse seaduses ettenähtud teose vaba kasutamise eesmärkidel ja tingimustel. Õppematerjalide kasutamisel on kasutaja kohustatud viitama õppematerjalide autorile.
Õppematerjalide kasutamine muudel eesmärkidel on lubatud ainult Tartu Ülikooli eelneval kirjalikul nõusolekul.
Tartu Ülikooli arvutiteaduse instituudi kursuste läbiviimist toetavad järgmised programmid:
euroopa sotsiaalfondi logo