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

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

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.

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

Forelæsninger, øvelser og obligatoriske afleveringsopgaver.