Hello,
I am struggling with the concept of resolution.
I understand that it applies to both propositional logic and fist order logic. I also understand that all first order logic needs to be converted to clause form (ie. remove implications, move Negation inwards (and adjust E to A and A to E), remove Existential qualifiers by using skolem functions. Remove universal quantifiers, and distribute to get () ^ () ^ () form of expression.
Now we are asked to prove G from our EXPRESSION. Hence we assume NOT G and try to see if we get a FALSE / NIL via resolution. For this we need to choose two clauses and resolve the negations inside it.
I have done some extra browsing on the internet - and will have to do some more reading in our book - but it seems linear resolution is the key.
We have from our previous exam paper:
1. Smoke(x) V ~Party(x) V Happy(x)
2. ~Single(y) V Party(Y)
3. Single(john)
4. ~Smoke(John)
5. ~Happy(Z) V Exciting(Z)
6. ~G: ~Exciting(W)
Thus i start with goal
Resolve G with 5 (only thing containing exciting) and we get
7. ~Happy(W) (i'm never sure which way around the substitution should go, but this seems correct to me). Lines 6 and 5
Now I resolve 7 with something from the KB (line 1)
8. Smoke(w) V ~Party(w)
Now I resolve 8 with something from KB (either 4 OR 2). I don't think I can resolve with 4, because I cannot replace JOHN with variable.
if I resolve with 2 I get : 9: ~Single(w) V Smoke(w)
Now I resolve 9 with something. I cannot resolve with 3 or 4 (it contains constants).
Where Am I going wrong?
Many thanks for your reply.
Danie
Danie van Eeden
------------------------
