Tillämpad logik

10 hp

Kursplan, Avancerad nivå, 1MA058

Det finns en senare version av kursplanen.
Kod
1MA058
Utbildningsnivå
Avancerad nivå
Huvudområde(n) med fördjupning
Datavetenskap A1N, Matematik A1N
Betygsskala
Underkänd (U), godkänd (3), icke utan beröm godkänd (4), med beröm godkänd (5)
Fastställd av
Teknisk-naturvetenskapliga fakultetsnämnden, 15 mars 2007
Ansvarig institution
Matematiska institutionen

Behörighetskrav

Kandidatexamen samt Logik och bevisteknik I och Automatateori eller motsvarande.

Mål

För godkänt betyg på kursen skall studenten

  • ha kännedom om oavgörbarheten av predikatlogik (Churchs sats);

  • ha kännedom om fullständighetssatserna för sats- och predikatlogik, och deras användning;

  • ha kännedom om och färdighet i metoder för effektiv representation och lösning av satslogiska problem;

  • ha färdighet i att formalisera problem i sats-, predikat- och modallogik;

  • ha kännedom om olika tolkningar av modallogiska operatorer och tillämpningar på modellkontrollproblem;

  • ha färdighet i modellteoretiska resonemang med predikat- och modallogik;

  • ha kännedom om kalkyler och system för automatisk bevissökning i predikatlogik;

  • ha kännedom om avgörbarhetsmetoder för ekvationell logik;

  • kunna använda något bevisstödssystem byggt på ett logiskt ramverk;

  • förstå 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, Gröbnerbasmetoder för polynomringar.

    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 och eventuellt muntligt prov vid kursens slut eventuellt kombinerat med inlämningsuppgifter under kursen enligt anvisningar som lämnas vid kursens start.

    • FÖLJ UPPSALA UNIVERSITET PÅ

    facebook
    instagram
    twitter
    youtube
    linkedin