0440949 - Andreas van Cranenburgh, excersizes 8

1. a: yes, b: no, c: say what?

5. [9.18, p. 318 R&N]
a. Horses are animals:
	@x Horse(x) -> Animal(x)
   The head of a horse is the head of an animal:
    	@h (\x HeadOf(h, x) & Horse(x)) -> (\x HeadOf(h, x) & Animal(x))

b. convert to CNF. premise: 
= !Horse(x) | Animal(x)

	conclusion: 
[eliminate implication]
=  @h !(\x HeadOf(h, x) & Horse(x)) | (\x HeadOf(h, x) & Animal(x))

[move ! inwards]
= @h (@x !HeadOf(h, x) | !Horse(x)) | (\x HeadOf(h, x) & Animal(x))

[eliminate quantifiers (+ skolemize)]
= (!HeadOf(h, x) | !Horse(x)) | (HeadOf(h, X1) & Animal(X1))
= (!HeadOf(h, x) | !Horse(x)) | (HeadOf(h, F(h)) & Animal(F(h)))

negate conclusion:
! (!HeadOf(h, x) | !Horse(x)) | (HeadOf(h, F(h)) & Animal(F(h)))
= (HeadOf(h, x) & Horse(x)) & (!HeadOf(h, F(h)) | !Animal(F(h)))

c. Resolutie:
{!Horse(x), Animal(x)} {HeadOf(h, x)} {Horse(x)} {!HeadOf(h, F(h), !Animal(F(h))}
     |                                   |                          /
      \_________________________________/                          /
                       |                                          /
     {Animal(x)} {HeadOf(h, x} {!HeadOf(h, F(h), !Animal(F(h))}  /
                                                       \________/
                                                            |
        	             {HeadOf(h, x} {!HeadOf(h, F(h)}  theta=UNIFY(x/F(h))
			              \        /
				       \______/
				           |
				          {}  theta=UNIFY(x/F(h))

6.













7a. {A, F(A), F(F(A)), ...}
b. {P(A) | !P(A),
P(F(A)) | !P(F(A)),
...}
c. each line is of the form P | !P, and thus a tautology, thus resolves with itself.
d.
e.
f. no
g.