CS 2800: Logik og beregning Forår 2019

Dette kursus giver en introduktion til formel logik og dens dybe forbindelser til databehandling. Logik præsenteres fra et beregningsteknisk perspektiv ved hjælp af ACL2 Sedantheorembevisningssystemet. Målet med kurset er at introducere fundamentale, grundlæggende metoder til modellering, design og ræsonnement om beregning, herunder propositionel logik, rekursion, induktion, ligningsmæssige ræsonnementer, termineringsanalyse, omskrivning og forskellige bevisteknikker. Vi viser, hvordan man bruger logik til at formalisere syntaks og semantik i det centrale ACL2s sprog, et simpelt LISP-baseret sprog med kontrakter. Derefter bruger vi ACL2s-sproget til formelt at ræsonnere om programmer, til at modellere systemer på forskellige abstraktionsniveauer, til at designe og specificere grænseflader mellem systemer og til at ræsonnere om sådanne sammensatte systemer. Vi undersøger også beslutningsprocedurer for fragmenter af logik af første orden, og hvordan sådanne beslutningsprocedurer kan bruges til at analysere modeller af systemer.

Forudsætningerne er en grundlæggende fortrolighed med funktionel programmering (CS 2500) og diskrete strukturer (CS 1800). Hvis du ikke har denne baggrund, skal du have tilladelse fra din underviser.

Studenter, der deltager i kurset, skal dagligt tjekke Piazza for meddelelser.