I am trying to learn the resolution technique for FOL. Please let me know my mistakes here. Thank you
I have the following First Order Logic sentences:
¬G(x)∨K(y,x)∨h(x) (1)
¬G(x)∨¬F(y)∨h(x) . (2)
¬G(x)∨¬A(x)∨F(x) . (3)
¬G(x)∨¬K(y,x)∨¬A(y)∨A(x) . (4)
Prove/Disapprove Argument
¬G(x)∨¬A(x)∨h(x)
Step one negating ¬G(x)∨¬A(x)∨h(x) -->
G(x)∧A(x)∧¬h(x)
I will get three clauses:
G(x) (5)
A(x) . (6)
¬h(x) . (7)
From here, how do I start with resolution? I did the following way:
Resolving (3) AND (4)
¬G(x)∨F(x)∨¬K(y,x)∨¬A(y) (8)
Resolving (1) AND (8)
¬G(x)∨¬A(y)∨h(x)∨F(x) (9)
Resolving (2) and (9) (Unification y/x)
¬G(x)∨¬A(x)∨h(x) (10)
Now resolving (10) with (5)
h(x)∨¬A(x) (11)
Now resolving (11) with (6)
h(x) (12)
Now resolving (12) with (7)
Null
Hence Proved
Please let me know
You did that all correctly!
Here is a tip though: Whenever you have clauses that contain just a single literal (these are called unit clauses), first try to resolve as smuch as possible using those unti clauses: it typically makes your life easier. For example, some of those first couple of resolutions you did involved a good number of literals on either side, and so it is easy to forget one (indeed it was not easy for me to check), but when you resolve with unit clauses it is almost impossible to make a mistake ... and the resulting clauses get smaller to boot, so things will get easier and easier.
Another good thing to know about is something called clause subsumption. A clause $C_1$ subsumes a clause $C_2$ when every literal in $C_1$ also occurs in $C_2$, i.e when $C_1 \subseteq C_2$. Since you are trying to figure out a way to make at least one of the literals in each clause true, it should be clear that if you succed in that for $C_1$, then you will have automatically succeded in that for $C_2$ as well. In other words, $C_2$ is not going to effect the outcome of the resolution process, and can be ignored or eliminated. You have a nice case of this: clause $6$ subsumes clause $4$, so you can totally ignore clause $4$!
Yet another 'trick' is to be on the lookout for literals that occur in some of the clauses but whose complement (the negation, basically) does not. Such literals are called pure literals. Again, since you are trying to make at least one literal true in each clause, we see that we can set those pure literals to true, and thus satisfy each clause containing that pure literal .... meaning that we can also just completely ognore any clauses with pure literals. You have a nice case of this as well: $K(y,x)$ occurs in clause $1$, but $\neg K(y,x)$ does not occur anywhere. Hence, we can completely ignore clause $1$ as well.
In sum, you should be able to derive the null clause from clauses $2,3,5,6$, and $7$, and this should be a good bit easier than what you had: give it a try!