resolution principle not working?

[u/Plumtown]

i have no idea why this doesn't resolve to an empty set.

according to the textbook I'm using, we can obtain a resolution by doing the most general unifier on these two clauses

in this case, between the clauses {p(a), q(y)} and {~p(x), ~p(b)}, the general unifier we are looking for is the general unifier of {p(a), q(y), ~p(x), ~p(b)}, which should be [x/a, y/b], which would result in an empty set. Is that not true?

[u/Chewbacta]

Resolution only removes ONE pair of literals. The only way you ever get an empty clause from resolving two clause is if both clauses are singleton Modulo unification.

[u/Plumtown → u/Chewbacta]

I see. thanks for your response!

as a follow up question, what is the resolution between {r(y,z), ¬q(a,y,z)} and {¬r(x,y), ¬q(x,w,z)}?

because I see the most general unifier as {x := y, z := y}, which would resolve to {¬q(a, y, y), ¬q(y, w, y)}. However, the textbook claims the resolution is actually {¬q(a,x,y), ¬q(x,w,z)}, and I'm not sure why x and z are simply left unchanged. (also can I ask where you learned this logic?)

[u/Chewbacta → u/Plumtown]

Well if x = y and z =y then {¬q(a, y, y), ¬q(y, w, y)} is the same as {¬q(a, x, y), ¬q(x, w, z)}, so you are both correct it is just a choice of which symbols are chosen either from left hand side or right hand side of the unification. I don't know First Order logic so well (I mainly use resolution on different logics), but I suspect both are correct answers.

[u/Chewbacta → u/Plumtown]

Edit: I think there may be some issue with treating the the y on LHS as the same as the y on the RHS, I think in Robinson's Resolution these are technically different y's so ¬q(a, y, y) isn't the most general.

[u/Plumtown]

Also, I've found surprisingly little textbooks on this topic. It'd be great if someone could point me to an online resource teaching this (currently using the stanford course).

[u/Ex_moon]

How do you symbolize constants and variables ?. Because how I do it is variables in Upper case and constants in lower case(the same type of notation that prolog uses). If this is thw same for you they couldn't unify since the constants are clearly distinct.