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å?