At give den studerende viden og forståelse for en række logiske tilgange, metoder og teknikker benyttet til specifikation, modellering og formel ræssonering i kunstig intelligens og multiagent-systemer.
Læringsmål:
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
forklare ideerne og principperne bag logisk specifikation og ræssonering i AI (kunstig intelligens) og MAS (multiagent-systemer)
afgøre den logiske korrekthed af et udsagnslogisk argument og foretage udsagnslogiske ræssonementer benyttende semantiske tableauer, naturlig deduktion og resolution
benytte klassisk første-ordens logik til vidensrepræsentation, problem-formalisering, og ræssonering i AI
forklare og anvende semantiske tableauer og naturlig deduktion i første-ordens logik til logisk deduktion og ræssonering
forklare og anvende metoderne fra første-ordens resolution til automatiseret deduktion
forklare de logiske problemer vedrørende model-checking og test af opfyldelighed i konteksten af ræssonering indenfor AI
beskrive de forskellige modallogikker benyttet i AI og MAS og forklare de grundlæggende elementer i Kripke-semantikker
vælge og anvende passende modallogiske sprog til vidensrepræsentation, problemanalyse og logisk ræssonering i forskellige områder af AI, inkl. temporal og epistemisk ræssonering
beskrive og anvende forskellige logiske systemer til formalisering af, og ræssonering omkring, individuel og fælles viden og strategiske evner i multi-agent systemer
forklare og anvende semantiske tableauer til test af opfyldelighed og logisk deduktion i modale, temporale og epistemiske logikker
individuelt udforske og vurdere den relevante litteratur
Kursusindhold:
Klassisk logik som sprog for problemspecifikation og ramme for ræssonering i AI. Klassiske deduktive systemer: naturlig deduktion, semantiske tableauer og resolution. Automatiseret ræssonering og anvendelser indenfor AI. Modale, temporale og epistemiske logikker til specifikation og ræssonering i AI. Logikker for specifikation og ræssonering i multiagent-systemer: logikker for viden, tro, intentioner, evner og handlinger af individuelle agenter og grupper af agenter. Semantiske tableauer til test af opfyldelighed og logisk deduktion i modale, temporale og epistemiske logikker.
Litteratur:
En kombination af forelæsningsnoter og andet materiale vil blive gjort tilgængelig i løbet af kurset.
