Enkeltfag Engelsk 5 ECTS

Automatiseret Ræsonnering

Overordnede kursusmål

Ræsonnering er evnen til at drage logiske slutninger. Formålet med kurset er at give de studerende en introduktion til automatiske og interaktive computersystemer til ræsonnering om matematiske teoremer samt egenskaber ved it-systemer. Det vil dække teoretisk indsigt samt praktiske færdigheder i relevante bevisassistenter.

See course description in English

Læringsmål

  • forklare de grundlæggende begreber introduceret i kurset
  • udtrykke matematiske teoremer og egenskaber ved it-systemer formelt
  • mestre bevissystemet naturlig deduktion
  • relatere førsteordenslogik, højereordenslogik og typeteori
  • konstruere formelle beviser i procedural stil og i deklarativ stil
  • bruge automatiske og interaktive computersystemer til automatiseret ræsonnering
  • evaluere troværdigheden af bevisassistenter og relaterede værktøjer
  • kommunikere løsninger på problemer på en klar og præcis måde

Kursusindhold

Bevissystemet naturlig deduktion, førsteordenslogik, højereordenslogik og typeteori. Formelle beviser i procedural stil og i deklarativ stil ved hjælp af automatiske og interaktive bevisførere. Bevisassistenten Isabelle i kunstig intelligens og datalogi.

Anbefalede forudsætninger

02156/02157/02180, Bevissystemer for førsteordenslogik, funktionsprogrammering, grundlæggende algoritmer i kunstig intelligens. Matematisk modenhed. Logikprogrammering er en fordel.

Undervisningsform

Forelæsninger, øvelser og obligatoriske afleveringsopgaver.

Fakultet

Se kurset i kursusbasen

Tilmelding

Sprog

Engelsk

Varighed

13 uger

Institut

Compute

Sted

DTU Lyngby Campus

Kursus ID 02256
Kursustype Kandidat
Semesterstart Uge 5
Semester slut Uge 19
Dage tors 13-17
Pris

7.500,00 kr.

0 pladser tilbage

Tilmelding