0440949 - Andreas van Cranenburgh, excersizes 9

1. a. @x dragon(x) -> ( @y parent(x, y) & fly(y) -> happy(x) )
b. @u ( green(u) & dragon(u) ) -> fly(u)
c. @v \w ( dragon(v) & parent(w, v) & green(w) & dragon(w) ) -> green(v)
conclusion: @z green(z) & dragon(z) -> happy(z)

to CNV: 
a. elim impl. @x !dragon(x) | @y !parent(x, y) | !fly(y) | happy(x)
   drop univ     !dragon(x) | !parent(x, y) | !fly(y) | happy(x)
b. elim impl. @u !green(u) | !dragon(u) | fly(u)
   drop univ.    !green(u) | !dragon(u) | fly(u)
c. @v \w ( dragon(v) & parent(w, v) & green(w) & dragon(w) ) -> green(v)
elim. impl. @v \w !( dragon(v) & parent(w, v) & green(w) & dragon(w) ) | green(v)
move ! inw.
        @v \w !dragon(v) | !parent(w, v) | !green(w) | !dragon(w) | green(v)
skolemize & drop univ.
	!dragon(v) & !parent(F(v), v) | !green(F(v)) | !dragon(F(v)) | green(v)

conclusion: 
negate		! (@z green(z) & dragon(z) -> happy(z))
eliminate impl	! @z ! ( green(z) & dragon(z) ) | happy(z)
move ! inw	\z ( green(z) & dragon(z) ) | happy(z)
skolem		( green(Z) & dragon(Z) ) | happy(Z)
distr | over &	( green(Z) | happy(Z) ) & (dragon(Z) | happy(Z))

!dragon(x) | !parent(x, y) | !fly(y) | happy(x)
!green(u) | !dragon(u) | fly(u)
dragon(v) & !parent(F(v), v) | !green(F(v)) | !dragon(F(v)) | !green(v)
( green(Z) | happy(Z) ) & (dragon(Z) | happy(Z))

2. (@x P(x) & ((@y P(y)) -> Q(x))) -> @x Q(x)
negation:
!((@x P(x) & ((@y P(y)) -> Q(x))) -> @x Q(x))
!(!(@x P(x) & (!(@y P(y)) | Q(x))) | @x Q(x))
(@x P(x) & (\y !P(y)) | Q(x))) & \x !Q(x)
(P(x) & (!P(Y)) | Q(x))) & !Q(Z)

{P(x)} {!P(Y), Q(x)} {!Q(Z)}
  \     /                 /
  {Q(x)} met theta={x/Y} /
    \                   /
      {} met theta={Y/Z}

\x P(x) & ((@y P(y)) -> Q(x)) -> @x Q(x)
CNV with negation:
!((\x P(x)) & ((@y P(y)) -> Q(x)) -> @x Q(x))
!(!(\x P(x)) & (!(@y P(y)) | Q(x))) | @x Q(x) )
( ! (\x P(x)) & (!(@y P(y)) | Q(x))) | @x Q(x) )
\x (P(x) & (!(@y P(y)) | Q(x)) & \x !Q(x)
\x (P(x) & (\y !P(y)) | Q(x)) & \x !Q(x)
(P(X) & (!P(Y)) | Q(X)) & !Q(Z)

{P(x)} {!P(Y), Q(x)} {!Q(Z)}
  \     /                 /
  {Q(Y)} met theta={x/Y} /
    \                   /
      {} met theta={Y/Z}

Exactly the same resolution.

3. the definition is: Result([a|seq], s) = Result(seq, Result(a, s))
thus it follows that the order is from right to left, since the action in the previous situation is taken as the first argument.

4a. Result([a], s) = Result(a, s)
follows from
Result([], s) = s
b.

5. No, it is stated that grabbing and holding is for the gold, and since the agent is not made of gold itself....

8. Having(arrow, s) -> Poss(Shoot(x), s)
Poss(Shoot(x), s) -> Shoot(direction), !Having(arrow, Result(Shoot(x), s))