HUMIT1750MN oppgaver uke 38
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? ND1750, 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 utsagn, inni parenteser. Finn ut hvilke regler dette systemet inneholder, og skriv dem, hvis mulig, opp i formatet som er brukt i boka (f.eks. i boksen side 371) og i arket som beskriver ND1750. 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??
Gj?r oppgavene 1, 2, 4, 5ab og 8 side 381?383 i l?reboka. Pr?v ? klare deg med reglene i ND1750. Bevis dessuten (ogs? i ND1750) implikasjonene ? (A ∨ B) → (? A ∧ ? B) og (? A ∧ ? B) → ? (A ∨ B) .
Bevis til slutt de to utsagnene (A → B) → ((B → C) → (A → C)) og (? C ∨ ? D) → ((A → C) → ((B → D) → (? A ∨ ? B))) i ND1750 uten bruk av reglene HS og DD. Forklar hvorfor dette viser at versjonene av ND1750 med og uten HS og DD er like sterke, det vil si at de lar oss bevise n?yaktig de samme utsagnene.