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 artificiell intelligens, databassystem och beräkningsteori. Under kursen skapas den här förtrogenheten genom att förmedla sats- och predikatlogikens begrepp och tekniker ur en datavetenskaplig synvinkel. Även temporal logik behandlas i samband med att modellteori diskuteras. Särskild vikt läggs på skillnaden mellan sanning och bevis, det vill säga definitionen av begreppet sanning å ena sidan och utvecklandet av formella system för att härleda sanningsvärdet av ett påstående å andra sidan.