| Dato | Undervises av | Sted | Tema | Kommentarer / ressurser |
| 23.01.2006 | Christian Mahesh Hansen, Roger Antonsen | Lille auditorium | Introduksjon, mengdelære, utsagnslogikk. | Husk obligatorisk oppmøte!Foiler for skjerm eller for utskrift: 4 på 1 | artikkelAktuelle avsnitt fra Gallier: 2.1.1 [Cartesian product = kryssprodukt], 2.1.2 [vi definerer funksjoner som totale funksjoner], 2.1.8, 3.1, 3.2.1. |
| 30.01.2006 | Christian Mahesh Hansen | Lille auditorium | Mengdelære (forstetter). Induktive definisjoner. Utsagnslogikk (fortsetter): syntaks, semantikk, induksjonsbevis, sekventkalkyle. | Fredag: oblig 1 utleveres.Foiler for skjerm eller for utskrift: 4 på 1 | artikkelAktuelle avsnitt fra Gallier: 3.3 [Hx i Gallier tilsvarer våre semantiske operatorer med hatt over. v med hatt over i Gallier tilsvarer våre boolske valuasjoner.], 3.4.1. |
| 06.02.2006 | Christian Mahesh Hansen | Lille auditorium | Utsagnslogikk (fortsetter): sekventkalkyle og sunnhet. | Foiler for skjerm eller for utskrift: 4 på 1 | artikkelAktuelle avsnitt fra Gallier: 3.4.1 ["deduction tree" = utledning], 3.4.2 [Gallier definerer sekventer der Gamma og Delta er sekvenser, i motsetning til våre multimengder. Galler bruker implikasjonstegn (venstrepil) der vi bruker sekventtegn. Gallier bruker en liggende U (med åpningen mot venstre) som implikasjonstegn. "inference rule" = slutningsregel. "principal formula" = hovedformel. "side formulae" = aktive formler.], 3.4.3, 3.4.4 [Galliers definisjon av aksiom krever ikke at felles formel A må være atomær. "proof tree" = bevis, "deduction tree" = utledning. Gallier definerer utledninger/bevis ved å starte med løvsekventene for deretter å generere nye konklusjoner nedover, altså det motsatte av hva vi gjør.], 3.4.5. |
| 13.02.2006 | Arild Waaler | Lille auditorium | Intuisjonistisk utsagnslogikk: syntaks og Kripke-semantikk. Sekventkalkylen LJ. Sunnhet av LJ med hensyn på Kripke-modeller. Konsistens. | Foiler for skjerm eller for utskrift: 4 på 1 | artikkelFredag: innleveringsfrist oblig 1. |
| 20.02.2006 | Roger Antonsen | Lille auditorium | Utsagnslogikk (fortsetter): kompletthet av LK. Førsteordens logikk: syntaks | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel Aktuelle avsnitt fra Gallier: 3.3.5 NP-Complete Problems, 3.4.7 Completeness of the Gentzen System G' [Gallier gjør kompletthet annerledes enn oss. Vår metode er en endelig versjon av hva som gjøres for første-ordens logikk.] 3.5.5 Hintikka Sets [Vår konstruksjon er Hintikkamengder i forkledning.] 5.1, 5.2.1-3 First-Order Logic |
| 27.02.2006 | Christian Mahesh Hansen | Lille auditorium | Førsteordens logikk: syntaks og semantikk | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel Fredag: oblig 2 utleveres. |
| 06.03.2006 | Roger Antonsen | Lille auditorium | Førsteordens logikk: semantikk og diverse | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel |
| 13.03.2006 | Roger Antonsen | Lille auditorium | Førsteordens logikk: sekventkalkyle og sunnhet | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel Fredag: innleveringsfrist oblig 2. |
| 20.03.2006 | -------- | -------- | -------- | Undervisningsfri uke. |
| 27.03.2006 | Roger Antonsen | Lille auditorium | Førsteordens logikk: kompletthet | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel Fredag: innleveringsfrist oblig 2.Fredag: oblig 3 utleveres. |
| 03.04.2006 | Christian Mahesh Hansen | Lille auditorium | Automatisk bevissøk: introduksjon, substitusjoner og unifisering | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel |
| 10.04.2006 | -------- | -------- | -------- | Påskeferie. |
| 17.04.2006 | -------- | -------- | -------- | Påskeferie.Fredag: innleveringsfrist oblig 3. |
| 24.04.2006 | Christian Mahesh Hansen | Lille auditorium | Automatisk bevissøk: fri-variabel sekventkalkyle og sunnhet | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel |
| 01.05.2006 | -------- | -------- | -------- | Offentlig høytidsdag. |
| 08.05.2006 | Herman Ruge Jervell | Lille auditorium | Snitteliminasjon | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel |
| 15.05.2006 | Christian Mahesh Hansen | Lille auditorium | Automatisk bevissøk: inkrementell lukking | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel |
| 22.05.2006 | Christian Mahesh Hansen | Lille auditorium | Automatisk bevissøk: matriser og koblingskalkyle | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel |
| 29.05.2006 | Roger Antonsen | Lille auditorium | Avanserte emner | Foiler for skjerm eller for utskrift: 4 på 1 | artikkel |
| 05.06.2006 | -------- | -------- | -------- | 2. pinsedag. |
| 12.06.2006 | Christian Mahesh Hansen, Roger Antonsen | Lille auditorium | Repetisjon | Foiler for skjerm eller for utskrift: 4 på 1 | artikkelHusk eksamen 14. juni! Det blir skriftlig eksamen i kurset. For mer informasjon, se her .Lykke til! |
Undervisningsplan
Publisert 2. jan. 2006 16:18
- Sist endret 12. juni 2006 18:17