FDD3029 Epistemisk logik 6,0 hp

En föreläsning á två timmar per vecka under 7 veckor. Inlämningar med aktuella ämnen varje vecka (betygsätts i omgångar om 2 veckor), ett hemtenta och ett praktiskt projekt.

Vi introducerar epistemisk logik, en modal logik som vi använder för att representera och resonera om kunskap formellt. Vi kommer att studera dess teoretiska grunder, inklusive möjliga världar-modeller och axiomatiseringar vars sundhet och fullständighet vi kommer att bevisa, och utforska tillämpningar inom områden som sträcker sig från matematiska gåtor till formella spel, distribuerade system och datorsäkerhet. Målet är att täcka större delen av kapitel 1-4 och delar av kapitel 5 i Reasoning about Knowledge, samt några nyare tillämpningar som tillkommit efter bokens publicering.

Kursen är grovt uppdelad i två halvor, med 4 veckor som täcker de brett tillämpningsbara teoretiska grunderna för epistemisk logik, och ytterligare 3 veckor som utforskar dess tillämpningar för en mängd olika problem inom datavetenskap inklusive distribuerade system och säkerhet.

Studenten skall kunna

• artikulera utmaningarna med att formellt representera kunskap, och förklara hur dessa hanteras med hjälp av epistemisk logik och möjliga världar-modellen av kunskap
• tolka epistemiska formler i möjliga världar-modellen
• bevisa och motbevisa tautologier med hjälp av både semantiska metoder och formell härledning av formler
• beskriva olika modeller och axiomatiseringar för modallogik, och bevisa att ett axiomsystem är sunt och fullständigt
• använda epistemisk logik för att formalisera och resonera om problem som involverar kunskap inom områden som programanalys, distribuerade system och protokoll samt spelteori
• förstå och implementera verktyg för automatiserade resonemang med epistemisk logik

Inga

Bekantskap med satslogik och matematiska bevis samt programmeringskunskaper i ett generellt programspråk.

Dator med fungerande programmeringsmiljö

Reasoning about Knowledge (Fagin, Halpern, Moses and Vardi), MIT Press 2004

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

• EXA1 - Examination, 6,0 hp, betygsskala: P, F

Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.

Examinator får medge annan examinationsform vid omexamination av enstaka studenter.

Kursen examineras utifrån 3 betygsatta inlämningar, en slutlig hemtentamen och ett programmeringsprojekt där studenten ska implementera en modellcheckare för epistemisk logik.

Musard Balliu

• Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
• Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
• Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.