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 

$x"yR(x,y) ? $y"xR(x,y)
og hvordan dette ga en prosess som aldri tok slutt.  F?lgende sekvent er heller ikke gyldig, men s?k etter bevis vil forl?pe annerledes:
 $x"yR(x,y) ? "x$yR(x,y)
P? hvilken m?te?  Pr?v ? si noe mest mulig generelt om hvorfor.

Enkelttimen

Last ned JFLAP hvis du ikke allerede har gjort det, og gj?r tutorialen om Finite Automata som du finner her. Skriv inn noen automater fra boken, gjerne dem du finner side 659 (denne er deterministisk) og 662 (denne er det ikke), og kj?r dem p? noen inputstrenger.