INF1800 oppgaver uke 37
Dobbeltimen (Tavle?velser)
Oppgave 5, 7ac, 8ac, 9ac, 10ac, 12ac, 13, 14ac og 15ac side 367?369 i l?reboken.
Oppgavene 1, 2, 4,og 5ab side 381?383 i l?reboken. Pr?v ? klare deg med reglene i ND1800. Bevis dessuten (ogs? i ND1800) implikasjonene ? (A ∨ B) → (? A ∧ ? B) og (? A ∧ ? B) → ? (A ∨ B) .
Enkeltimen (PC-?velser)
Gj?r deg kjent med teorembeviseren hos Gateway to logic: Det vil si, tast inn noe du tror er en tautologi og velg Prove the proposition i menyen Task to be performed. Du kan for eksempel skrive inn formler som blir bevist i dette notatet. Du vil f? ut beviser i et system for naturlig deduksjon som ligner ganske mye p? ND1800, men med litt andre regler. (Til dels har de bare andre navn.) Bevisene skrives i nesten samme format som i notat i lenken over, og som vi har sett p? forelesningene; eneste forskjell (utover at de dropper indenteringer) er at kolonnen som viser avhengigheter er flyttet helt til venstre, og kolonnen med linjenumre st?r helt inntil kolonnen med formlene, inni parenteser. Finn ut hvilke regler dette systemet inneholder, og skriv dem, hvis mulig, opp i formatet som er brukt i boken (f.eks. i boksen side 371) og i arket som beskriver ND1800. Finner du noen regler av samme type som v?re CP og IP, det vil si regler som eliminerer avhengigheter? Jeg har selv funnet 2. Fors?k ? gi generelle beskrivelser av disse reglene ogs?.
Systemet produserer i mange tilfeller un?dvendig lange og noks? kl?nete beviser. Dette er fordi det bruker en noks? enkel, generell strategi for ? finne beviser. Klarer du ? se omtrent hva denne strategien g?r ut p??