Not sure if this is really MPSIMS, but I wasn’t sure where to put it.
Okay, I’m playing around with using resolution on predicate logic as a way of solving one of those logic puzzle thingies (you know, the ones where you get a bunch of clues and have to match up 3 or 4 thingies and you get a grid layout to assist your deductive processes?). I just learnt predicate logic at universtity this semester, and I thought that the whole idea of resolution had finally clicked for me, but I’ve run across something that is troubling me.
I’ve got the following clauses (and a bunch of others not relevent):
{~R(p[sub]8[/sub], Hostelry, x[sub]8[/sub]), ~R(Sinclair, a[sub]8[/sub], y[sub]8[/sub]), ((y[sub]8[/sub] + 375) = x[sub]8[/sub])}
{R(f[sub]11[/sub](b[sub]11[/sub]), b[sub]11[/sub], t[sub]11[/sub](b[sub]11[/sub])}
{R(p[sub]10[/sub], o[sub]10[/sub](p[sub]10[/sub]), t[sub]10[/sub](p[sub]10[/sub])}
(I’m using slightly non-standard notation here I think; the ~ is not, and the full words are constants, the subscripted lowercase letters are variables and the subscripted lowercase letters with brackets after them are functions, while the uppercase letters with brackets after them are predicates. The exceptions to that being that I’m using the regular symbols and infix notation for the function ‘+’ and the predicate ‘=’.)
The puzzle involved 6 people travelling 6 different distances to set up 6 different businesses. R is a predicate defining the relationship between these things, i.e. R(p, b, x) is true if person p travelled x miles to set up business b.
The first clause came from a clue saying that “The person who owns the hostelry travelled 375 more miles than Sinclair”, and the clause roughly translates into english as “Either the hostelry owner didn’t travel x[sub]8[/sub] miles, or Sinclair didn’t travel y[sub]8[/sub] miles, or x[sub]8[/sub] is y[sub]8[/sub] + 375”. Correct translation, n’est-ce pas?
The 2nd and 3rd clauses come from the structure of the game, the original logic formulae translated into English as “for every business there exists a person who owns that business and a distance that person travelled” and the analagous thing for people instead of businesses. After being translated into clausal form they read “for every business the owner of the business owns the business and the distance its owner travelled is the distance its owner travelled”, which is also correct, isn’t it?
Now, here comes the weird part.
I can substitute stuff in clauses 1 & 2 and then resolve on the R(…) and ~R(…), and then do the same with the resolvent of that and clause 3, to finally get
{(y[sub]8[/sub] + 375) = x[sub]8[/sub]}
Now, this isn’t falsum, and my text book doesn’t say that proves that the original stuff was inconsistent (good, 'cause I’m not doing a refutation proof!), but it is blatantly false (reads as “for any two numbers the second is the first plus 375”, which isn’t even true for the restricted set of 6 numbers I’ve got).
This is confusing my poor addled brain. One thing I think could be the problem is that in my substitutions I put variables in place of functions of variables (x[sub]8[/sub] instead of t[sub]11/sub for example)… is that wrong? I couldn’t find the answer to that in my text book. However, if not I could just substitute the other way couldn’t I? In which case I’d end up with a clause saying something like “for every business and person, the distance travelled by the owner of the business is 375 + the distance travelled by the person”, which is also blatantly false.
I’m quite sure I’m either doing something wrong, or I just haven’t quite got the concept properly. If there’s anyone out there who has a clue what I’m talking about, and is able to explain it to me (preferably the one word a page and with pictures version), I would be extremely grateful.
And what are the rest of you looking like that for? I warned you it would be boring.