F=föreläsning, L=lektion. I sal 1145 om ej
annat anges.
| Dag | tid, lokal | Planerat innehåll | Material |
| Ti 5/9 | 13-15 F | Icke-konstruktiva bevis. Lambdakalkyl.
Algoritmisk tolkning av logiska konnektiv. |
Konstruktiv logik,
kap. 1-4 Övn.blad 1 |
| To 7/9 | 10-12 F | Intutionistisk logik. Curry-Howard isomorfin | |
| " | 13-15 L | Räkneövning (övn.blad 1) | Facit till Övn.
blad 1. |
| Ti 12/9 | 13-15 F | Förhållande mellan klassisk och intuitionistisk logik.
Martin-Löfs typteori: påstånden-som-typer, beroende typer, pi- och sigmatyper. |
Konstruktiv logik,
kap 5-8. Övn.blad 2 +facit Lab.anvisn. 1 |
| To 14/9 | 10-12 F | Typteori: induktiva typer. Typteori och funktionell
programmering. Universum. Bevisstödssystem (Agda/Alfa). |
|
| " | 13-15 L alt. labb i 1357
(L. Lindqvist) |
Räkneövning/laboration (övn.blad 2, lab. 1) | |
| Ti 19/9 | 13-15 F | Modallogik och Kripkemodeller. | Konstruktiv logik,
kap 9. Övn.blad 3 +facit Lab.anvisn. 2 |
| To 21/9 | 10-12 F | Termomskrivningssystem: universell algebra,
fullständighet för ekvationella teorier. |
Kompl. material om
termomskrivningssystem. Delar av "Term rewriting system" (Klop). |
| " | 13-15 L
(L. Lindqvist) |
Räkneövning (övn.blad 3) | |
| Må 25/9 | 13-15 labb 1412-4
(L. Lindqvist) |
Laboration (lab 1-2) | |
| Ti 26/9 | 13-15 F i sal 1246 | Termomskrivningssystem: konfluens, stark normalisering.
Termineringsbevis. |
Delar av "Term rewriting
systems" (Klop) Övn.blad 4 |
| To 28/9 | 10-12 F | Välkvasiordningar. Kruskals sats.
Knuth-Bendix komplettering, unifiering, kritiska par. |
|
| " | 13-15 L | Studentpresentation av lösta uppgifter. | |
| Må 2/10 | 13-15 F | Inledning till automatisk bevisföring. Tablåkalkylen.
Sekventkalkylen. Satslogisk fullständighet.. Delformelegenskapen. |
Sigstams kompendium
(säljes)
Övn.blad 5 |
| To 5/10 | 10-12 F | Fullständighetssatsen för predikatlogik.
Bevisökning i sekventkalkylen. Konsekvenser av fullständighetssatsen. |
Facit övn.blad 4
Övn.blad 6 |
| " | 13-15 L | Studentpresentation av lösta uppgifter + Räkneövning | |
| Må 9/10 | 13-15 F | Resolution m.fl. praktiska metoder. | Resolution Theorem Proving. The propositional proof formula checker HeerHugo. Övn.blad 7 |
| Ti 10/10 | 13-15 F | Algoritmer för satslogiska problem: 2-CNF och
Davis-Putnams metod. Stålmarcks metod. |
Decidable Theories. läsanvisning för kursen. |
| To 12/10 | 13-15 L | Studentpresentation av lösta uppgifter + Räkneövning | Facit till övn.blad 5,6,7. |
| Fr 13/10 | 10-12 F | Avgörbara och oavgörbara teorier. Kvantorelimination.
Reduktion av problem till avgörbara teorier. |
Övn. blad 8 |
| Må 16/10 | 13-15 F | Gästföreläsning av Tekn.Dr. Lars-Henrik Eriksson,
Industrilogik AB. |
|
| Ti 17/10 | 10-12 F | Avgörbarhet av algebraiska och geometriska problem. | |
| On 18/10 | 10-12 L i sal 1245 | Räkneövning |
Tenta: 20/10 kl. 8-13 Magistern, Sal A (Dag Hammarskjölds väg 31,
tel 471 73 37)