Behörighetskrav

120 hp med kurserna Logik och bevisteknik I och Automatateori eller motsvarande. Engelska 6. (Med en svensk kandidatexamen uppfylls kravet på engelska.)

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.

Om särskilda skäl finns får examinator göra undantag från det angivna examinationssättet och medge att en enskild student examineras på annat sätt. Särskilda skäl kan t.ex. vara besked om särskilt pedagogiskt stöd från universitetets samordnare för studenter med funktionsnedsättning.