02256 Automatiseret Ræsonnering

2022/2023

Kursusinformation
Automated Reasoning
Engelsk
5
Kandidat
Kurset udbydes som enkeltfag
F4B (fre 8-12)
Campus Lyngby
Forelæsninger, øvelser og obligatoriske afleveringsopgaver.
13-uger
F4B
Skriftlig eksamen og bedømmelse af rapport(er)
Bedømmes som en helhed.
Skriftlig eksamen: 2 timer
Alle hjælpemidler er tilladt
7-trins skala , ekstern censur
02156.02157.02180 , Bevissystemer for førsteordenslogik, funktionsprogrammering, grundlæggende algoritmer i kunstig intelligens. Matematisk modenhed. Logikprogrammering er en fordel.
Jørgen Villadsen , Lyngby Campus, Bygning 322, Tlf. (+45) 4525 3733 , jovi@dtu.dk
01 Institut for Matematik og Computer Science
https://courses.compute.dtu.dk/02256/
I studieplanlæggeren
Kontakt underviseren for information om hvorvidt dette kursus giver den studerende mulighed for at lave eller forberede et projekt som kan deltage i DTUs studenterkonference om bæredygtighed, klimateknologi og miljø (GRØN DYST). Se mere på http://www.groendyst.dtu.dk
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.
Læringsmål
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
  • 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.
Sidst opdateret
01. juni, 2022