Oppgaver uke 42
Dobbeltimen
Oppgave 4,5,6 fra eksamen i HUMIT1750 høsten 2005, men bruk sekventkalkyle i oppgave 4. Du skal altså bevise sekventen Þ A, der A er formelen i oppgave 4.
Skriv ferdig bevisene for sekventene
"x R(x,f(x)), "x"y"z (R(x,y) Ù R(y,z) ® R(x,z)) Þ "x R(x,f(f(x)))
og
"x (ku(x) ® kd(x)), "x (kd(x) ® d(x)), "x (kd(x) ® veg(x)), "x (veg(x) ® ¬ $y (d(y) Ù s(x,y))) , ku(d) Ù ku(l) Þ ¬ s(d, l)
som vi begynte på på forelesningen 2/10. Hadde det vært mulig å gjennomføre det siste beviset ved å bruke første versjon av kvantorreglene? Hvorfor/hvorfor ikke?
Siste sekvent er ikke gyldig hvis vi erstatter ku(d) Ù ku(l) med ku(d) Ú ku(l). Kan vi være sikre på at et bevissøk etter retningslinjene skissert i notatet og på forelesningen 3/10 vil stoppe? For å forenkle denne siste oppgaven kan du, hvis du vil, heller se på et tilsvarende tilfelle der du har skrevet om alle formlene til preneks normalform.
På forelesningen 3/10 så vi på bevissøk for den ugyldige sekventen