Grundläggande logik och modellteori

Kursen tar upp satslogik, predikatlogik och modellteori. Under kursen behandlas begrepp som syntax, semantik, bevis, sundhet och fullständighet, likhet, Horn-formler, unifiering och resolution.

Det krävs förtrogenhet med formella logiska system för att förstå grundläggande begrepp inom många datavetenskapliga områden såsom databaser, vetenskapliga beräkningar och maskininlärning. Modul 1 skapar den här förtrogenheten genom att förmedla logikens begrepp och tekniker ur en datavetenskaplig synvinkel.

Särskild vikt läggs på (i) skillnaden mellan logiskt sanna påståenden och bevis, dvs. definitionen av begreppet logisk sanning å ena sidan och utvecklandet av formella system för att härleda sanningsvärdet av ett påstående å andra sidan, (ii) algoritmiska aspekter på bevissystem med tonvikt på resolution och (iii)  modeller för logiska system och hur dessa används för att verifiera egenskaper.

Modul 2 ger färdighetsträning inom logik genom ett antal obligatoriska uppgifter. Modulen illustrerar teori från modul 1, exempelvis genom uppgifter i logikprogrammering och ger studenten möjligheten att använda definitioner, notationer och formella system i praktiken.