Kursbeskrivning

Kursen ger en introduktion till matematisk logik och dess tillämpningar inom datalogi. Du får lära dig:

• använda logik för att formalisera egenskaper hos datastrukturer, algoritmer och datorsystem
• genomföra bevis för att härleda slutsatser utifrån givna premisser
• behärska olika bevistekniker, såsom naturlig deduktion, induktion. s.k. Hoare-logik för programverifikation, och temporal-logik för systemverifikation
• förstå hur logiska formler kan ges en precis matematisk (modell-teoretisk) innebörd
• behärska grunderna för automatisk deduktion
• förstå och resonera kring viktiga egenskaper hos bevissystem, såsom sundhet, fullständighet och avgörbarhet