| Dato | Undervises av | Sted | Tema | Kommentarer / ressurser |
| 23.08.2005 | Tore Langholm | Oversikt over kurset, samt gjennomgang av 1.1 og 1.2. (Unntak: 1.1.2 er kursoriks pensum. 1.1.3 er ikke pensum. 1.2.4 er ikke pensum. 1.2.5 er kursorisk pensum.) | Det er første gang kurset foreleses etter Heins lærebok, og den nøyaktige fremdriftsplanen kan bli endret underveis. Tall som 1.1 etc. henviser til deler av kapitler i læreboken.Denne dagen foreleste jeg fra 1.1 (første time) og 1.2 (andre time), men jeg gikk ikke gjennom alt stoffet, spesielt gikk jeg ikke gjennom bokens eksempler. Dette må leses på egenhånd. Lysark fra første time finnes her som henholdsvis pdf-dokument og powerpoint-presentasjon. Legg spesielt merke til lenken til slutt, gjengitt her . Trykk på den grå knappen merket Start Truth Table Constructor nede til høyre på siden du da kommer til, og prøv deg frem ved for eksempel å skrive inn ((A v B) => C) <=> ((A => C) ^ (B => C)) i vinduet oppe til venstre og deretter trykke OK. | |
| 25.08.2005 | 1.3.3 | Lysark (bare for første del av forelesningen!) finnes her som henholdsvis pdf-dokument og powerpoint-presentasjon. | ||
| 30.08.2005 | 1.3.1, 1.3.4, 2.1.1 | Vi snakker om disse begrepene. | ||
| 01.09.2005 | "Matematisk induksjon. Kapittel 3 til og med 3.1.1, samt utdrag fra 4.4.1 | Kapittel 3 til og med 3.1.1, samt utdrag fra 4.4.1. Rammen side 255 har dette spesialtilfellet for naturlige tall. Ta også en kikk på de to animasjonene tilgjengelige fra lenkene 1a. Principle of Mathematical Induction animation og 1b. Example of Mathematical Induction animation her | ||
| 06.09.2005 | 6.1 og 6.2 | Gjelder hele uken. Lysark som Powerpoint eller i pdf | ||
| 08.09.2005 | ||||
| 13.09.2005 | 6.3 | Vi tok for oss begrepene aksiom, slutningsregel, bevis og bevis fra premisser, og gikk gjennom en del eksempler. Vi oppdaget også en liten feil i boken som ikke står i errata-listen: I beviset side 375 slutter man fra B i linje 2 til AvB i linje 3 ved hjelp av noe som oppgis å være slutningsregelen Add. Men slik denne regelen presenteres side 371, lar den oss bare slutte AvB fra den første disjunkten, altså A. For å få dette til å gå i hop, må vi derfor utvide definisjonen side 371 slik at Add også tillater oss å slutte fra B til AvB. Tilsvarende (for å få til overgangen fra linje 4 til linje 5 side 375) må vi også legge inn en ekstra versjon av Simp, som tillater oss å slutte fra A&B til den andre konjunkten B. | ||
| 15.09.2005 | 6.3 fortsatt. | Vi så blant annet på beviser ved såkalt reductio ad absurdum, det vil si beviser som bruker regelen IP.Flere av temaene vi har vært innom til nå er illustrert på nettstedet Gateway to Logic (Gå gjerne rett videre til lenken Server-side functions ) Her kan man skrive inn en formel og se dens sannhetsverditabell, få den skrevet om til DNF, etc. Man kan også få den bevist hvis den er en tautologi. Da brukes et natural deduction-system som likner på det som beskrives i vår lærebok. Alle bevis som returneres bruker regelen RAA, som essensielt er det samme som vår IP. Legg merke til at bevisene ofte er unødvendig lange og klønete; dette er fordi de genereres automatisk etter nokså enkle regler. | ||
| 20.09.2005 | 6.4 | Gjelder hele uken. Lysark som powerpoint eller i pdf | ||
| 22.09.2005 | Se over | Lysark som powerpoint eller i pdf ND1750 er vår presiserte versjon av "naturlig deduksjon" fra avsnitt 6.3. Dette systemet er komplett, som vi skal se i neste ukes øvelser. | ||
| 27.09.2005 | 7.1 | Gjelder hele uken.Vi begynner altså på predikatlogikk. Kikk gjerne på denne teorembeviseren hos "Gateway to Logic". Syntaksen er tilpasset vanlig tastatur, men skulle ellers ikke være vanskelig å sammenlikne med bokens. Skriv inn formler som du mener burde være gyldige/ikkegyldige, og se om systemet er enig.Lysark fra første halvpart av forelesningen i powerpoint og pdf | ||
| 29.09.2005 | Se over | Powerpoint. PDF. | ||
| 04.10.2005 | 7.2 | Powerpoint PDF | ||
| 06.10.2005 | 7.2 fortsatt. Vi begynner på 7.3. | Powerpoint PDF Eksempler på oversettelse til predikatlogikk | ||
| 11.10.2005 | Vi fortseter med 7.3 | Notatet med rettelser har svært mange referanser til avsnitt 7.3. Legg spesielt merke til at t is free to replace x in W nå (i motsetning til i boken) betyr at ingen fri forekomst av x i W står i skopet til en kvantor for en variabel i t. Til tross for rettelsene er bevisene som står etter reglene UI (7.15), EI (7.17), UG (7.18) og CP (7.19) dessverre fremdeles forvirrende, uklare og til dels gale, og utgår derfor fra pensum.Det som er viktig å lære seg, er hvordan reglene side 451 i boken leses og brukes. Se lenke til rettet versjon i ruten under. | ||
| 13.10.2005 | Vi avrunder 7.3 | Notat om premisser i bevis. ND1750PRED er vår rettete versjon av bevissystemet i avsnitt 7.3. | ||
| 18.10.2005 | 1.3.3, 11.1, litt av 11.2.1 | Lysark om regulære uttrykk. (Som PDF. )Lysark om DFAer. (Som PDF. )Vi rakk også å definere NFAer.The Regex Coach finnes på maskinene på Hundremeterskogen, og er et nyttig hjelpemiddel til å bli kjent med regulære uttrykk. Tilgjengelig herfra. En annen nyttig applikasjon er JFLAP; se denne lenken for informasjon om hvordan du kan få tak i (og kjøre) dette. | ||
| 20.10.2005 | resten av 11.2.1, litt av 11.2.2 | Om å lage automater fra regulære uttrykk og omvendt. Eksemplene 11.13 og 11.14 er ikke pensum. | ||
| 25.10.2005 | 11.2.5 og 11.3.2 | Notat of krav til DFAer i powerpoint og pdf. Endelige automater som produserer output. Konstruksjon av DFA fra NFA. | ||
| 27.10.2005 | 11.3.3 | Konstruksjon av minimal DFA. Lysark som powerpoint og pdf. Liten og stor DFA som vi minimaliserte på forelesningen. Dette er filer som kan leses av JFLAP; last dem ned og åpn dem fra JFLAP. Se også PDF-filer som viser minimalisering av den siste; først inndeling i grupper av ekvivalente tilstander og deretter inntegning av transisjoner. | ||
| 01.11.2005 | 11.4.2. Begynner på 3.3. | Siste halvpart av side 692 er ikke pensum. Siste linje side 179, side 180 og første halvpart av side 181 er ikke pensum. | ||
| 03.11.2005 | Avslutter 3.3. 11.4.1 | Lysark om kontekstfrie og regulære grammatikker i powerpoint og PDF. | ||
| 08.11.2005 | Kap. 12 t.o.m. 12.2.2. | Følgende deler av dette er kursorisk pensum: Fra midt på s. 704 til midt på s. 707, og fra midt på s. 709 til midt på s. 711. | ||
| 10.11.2005 | 12.4 | Repetisjon: Lysark om forholdet mellom endelige automater og regulære gramatikker i powerpoint og PDF.Lysark om venstrerekursjon i powerpoint og PDF.Tema ellers blir eliminasjon av lambda-produksjoner, samt Chomsky og Greibach normalform. | ||
| 15.11.2005 | Resten av 12.4. (Pumpelemma og lukningsegenskaper for kontekstfrie språk.) 13.1 (Innledende om turingmaskiner.) | |||
| 17.11.2005 | 13.1.2 | Eksempler på turingmaskiner i powerpoint og PDF, og som JFLAP-kjørbare filer: strengreversering, suksessorfunksjon med unær og binær tallrepresentasjon og konverteringsfunksjoner fra unær til binær og binær til unær representasjon. (De fem siste bør lastes ned før de kjøres, og gis navn som ender på ".jff".) | ||
| 22.11.2005 | 13.1.3 og 13.1.4 | Fra 2/3 ned på side 770 til 1/3 ned på side 773 er ikke pensum | ||
| 24.11.2005 | 13.2 unntatt 13.2.4. 14.2 | Lysark i powerpoint og PDF. Kontekstsensitiv og ubegrenset grammatikk i JFLAP-format for språket an bn cn. | ||
| 29.11.2005 | 14.1 | Det som står i 14.1 etter midten av side 798 er ikke pensum. | ||
| 01.12.2005 | Oppsummering | Vi ser kanskje også på en gammel eksamen. Tidligere var det to eksamener i dette kurset, førtst en to-timers eksamen i logikkdelen (eksempel og delvis løsningsforslag ) og så en tre-timers eksamen som fortrinnsvis dekket beregnbarhetsdelen. (Eksempel og løsningsforslag. ) (En til, med delvise løsningsforslag til spørsmål TO (endelig automat ), TRE (grammatikk ), og FIRE (turingmaskin ).)Vi brukte samtidig en annen lærebok med litt annet pensum og litt andre begreper og definisjoner. Regn derfor ikke med å forstå alt. |
Undervisningsplan
Publisert 30. mai 2005 16:12
- Sist endret 3. des. 2005 00:07