URL: www2.math.uu.se/~palmgren/tillog/schema01.html
F=föreläsning, L=lektion. I sal 1145 om ej
annat anges.
| Dag | tid, lokal | Planerat innehåll | Material |
| Må 3/9 | 13-15 F | Avgörbara och oavgörbara problem. Hilberts program. | Oavgörbara problem
i elementär aritmetik (EP) |
| Ti 4/9 | 13-15 F | Icke-konstruktiva bevis. Lambdakalkyl.
Algoritmisk tolkning av logiska konnektiv. |
Konstruktiv logik (EP),
kap. 1-4 Övn.blad 1 |
| To 6/9 | 13-15 F | Intutionistisk logik. Curry-Howard isomorfin | |
| Fr 7/9 | 13-15 L | Räkneövning (övn.blad 1) | |
| Må 10/9 | 13-15 F sal 1113 |
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. |
| Ti 11/9 | 13-15 F | Typteori: induktiva typer. Typteori och funktionell
programmering. Universum. Bevisstödssystem (Agda/Alfa). |
|
| " | 15-17 lab
sal 1412,1413 |
Laboration med Alfa | |
| To 13/9 | 13-15 F/L | Typteori forts. | |
| Fr 14/9 | 10-12 F | Modallogik och Kripkemodeller. | Konstruktiv logik,
kap 9. |
| Ti 18/9 | 13-15 L | Räkneövning | Övn. blad 2, 3, 4. |
| To 20/9 | 13-15 L | Termomskrivningssystem: universell algebra,
fullständighet för ekvationella teorier. |
Kompl. material om
termomskrivningssystem. Delar av "Term rewriting system" (Klop). |
| Fr 21/9 | 13-15 F sal 1113 |
Termomskrivningssystem: konfluens, stark normalisering.
Termineringsbevis. |
Delar av "Term rewriting
systems" (Klop) |
| Må 24/9 | 13-15 F | Välkvasiordningar. Kruskals sats.
Knuth-Bendix komplettering, unifiering, kritiska par. |
|
| Ti 25/9 | 13-15 lab sal 1412, 1413 |
Avslutande laboration i Alfa | |
| To 27/9 | 10-12 F | Inledning till automatisk bevisföring.
Sekventkalkylen. Satslogisk fullständighet. Delformelegenskapen. |
Fullständighetssatsen via
sekventkalkylen ... (Sigstam) |
| To 27/9 | 13-15 L | Studentpresentation av lösta uppgifter. | Problem 1 |
| Må 1/10 | 15-17 F sal 1113 |
Fullständighetssatsen för predikatlogik.
Bevissökning i sekventkalkylen. Konsekvenser av fullständighetssatsen. |
|
| To 4/10 | 15-17 F | Resolution m.fl. praktiska metoder. | Resolution Theorem Proving. |
| Fr 5/10 | 13-15 L sal 1113 |
Avgörbara och oavgörbara teorier. Kvantorelimination.
Reduktion av problem till avgörbara teorier. |
Oavgörbara problem ... (EP)
Utdrag ur Smorynski. |
| Må 8/10 | 13-15 F | Räkneövning | Övn. blad 5, 6, 7 |
| To 11/10 | 15-17 L |
Gästföreläsning: univ. lektor Lars-Henrik Eriksson, IT institutionen, avd. Datalogi |
|
| Må 15/10 | 13-15 L | Studentpresentation av lösta uppgifter | Problem 2 |
| Må 15/10 | 15-17 L sal 1113 |
Räkneövning eller räknestuga | Övn. blad 7 |
Tentamen: Onsdag 17/10 kl. 9-14, Polacksbacken.