Behörighetskrav

120 högskolepoäng med kurserna Logik och bevisteknik I och Automatateori eller motsvarande.

Mål

Efter godkänd kurs ska studenten kunna

• redogöra för oavgörbarheten av predikatlogik (Churchs sats);
• formulera fullständighetssatserna för sats- och predikatlogik samt kunna redogöra för deras användning;
• använda och beskriva metoder för effektiv representation och för lösning av satslogiska problem;
• formalisera problem i sats-, predikat- och modallogik;
• redogöra för olika tolkningar av modallogiska operatorer och tillämpningar på modellkontrollproblem;
• föra modellteoretiska resonemang med predikat- och modallogik;
• redogöra för någon kalkyl och för system för automatisk bevissökning i predikatlogik;
• redogöra för några avgörbarhetsmetoder för ekvationell logik;
• använda något bevisstödssystem byggt på ett logiskt ramverk;
• redogöra för algoritmisk tolkning av intuitionistisk logik, samt principer för programextraktion från bevis.

Innehåll

Satslogik: Kombinatoriska problem som satslogiska problem. Metoder för effektiv lösning och representation av satslogiska problem (Davis-Putnam, BDDer).

Modal logik: möjligavärldarsemantik, Kripke-modell.

Tolkningar av modal logik: Tidslogik och epistemisk logik. Tillämpning på modellkontroll.

Ekvationell logik: termer, unifiering, universell algebra, ekvationella resonemang, termomskrivning, Knuth-Bendix-komplettering, välordningar och termineringsbevis.

Predikatlogik och bevissökning: fullständighetssatsen, bevissökning i några kalkyler (Tableaux, resolution).

Lösbara och olösbara problem: fullständiga och avgörbara teorier, kvantorelimination, Gödels ofullständighetssats (ej bevis).

Konstruktiv logik och typteori: lambdakalkyl, enkel typteori, intuitionistisk logik, Martin-Löfs typteori, påståenden som datatyper, programextraktion från bevis, logiska ramverk, bevisstödssystem (Coq, Hol, Isabelle eller Agda).

Undervisning

Föreläsningar, räkneövningar och laborationer.

Examination

Skriftligt prov vid kursens slut kombinerat med inlämningsuppgifter under kursen enligt anvisningar som lämnas vid kursens start.