Dette emnet er erstattet av IN3070 – Logikk.

Undervisningsplan

DatoUndervises avStedTemaKommentarer / ressurser
23.01.2006Christian Mahesh Hansen, Roger Antonsen  Lille auditorium  Introduksjon, mengdelære, utsagnslogikk.  Husk obligatorisk oppmøte!

Foiler for skjerm eller for utskrift: 4 på 1 | artikkel

Aktuelle 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.2006Christian 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 | artikkel

Aktuelle 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.2006Christian Mahesh Hansen  Lille auditorium  Utsagnslogikk (fortsetter): sekventkalkyle og sunnhet.  Foiler for skjerm eller for utskrift: 4 på 1 | artikkel

Aktuelle 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.2006Arild 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 | artikkel

Fredag: innleveringsfrist oblig 1. 

20.02.2006Roger 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.2006Christian 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.2006Roger Antonsen  Lille auditorium  Førsteordens logikk: semantikk og diverse  Foiler for skjerm eller for utskrift: 4 på 1 | artikkel  
13.03.2006Roger 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.2006Roger 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.2006Christian 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.2006Christian 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.2006Herman Ruge Jervell  Lille auditorium  Snitteliminasjon  Foiler for skjerm eller for utskrift: 4 på 1 | artikkel 
15.05.2006Christian Mahesh Hansen  Lille auditorium  Automatisk bevissøk: inkrementell lukking  Foiler for skjerm eller for utskrift: 4 på 1 | artikkel  
22.05.2006Christian Mahesh Hansen  Lille auditorium  Automatisk bevissøk: matriser og koblingskalkyle  Foiler for skjerm eller for utskrift: 4 på 1 | artikkel 
29.05.2006Roger Antonsen  Lille auditorium  Avanserte emner  Foiler for skjerm eller for utskrift: 4 på 1 | artikkel  
05.06.2006--------  --------  --------  2. pinsedag. 
12.06.2006Christian Mahesh Hansen, Roger Antonsen  Lille auditorium  Repetisjon  Foiler for skjerm eller for utskrift: 4 på 1 | artikkel

Husk eksamen 14. juni!

Det blir skriftlig eksamen i kurset. For mer informasjon, se her .

Lykke til! 

Publisert 2. jan. 2006 16:18 - Sist endret 12. juni 2006 18:17