Resolution in First Order Logic I saw this question in a textbook and I have tried solving it but its proving too difficult to solve. Anyone here who can assist?
"Victor has been murdered, and Arthur, Bertram, and Carleton are the only suspects (meaning exactly one of them is the murderer). Arthur says that Bertram was the victim’s friend, but that Carleton hated the victim. Bertram says that he was out of town the day of the murder, and besides he didn’t even know the guy. Carleton says that he saw Arthur and Bertram with the victim just before the murder. You may assume that everyone – except possibly for the murderer – is telling the truth. (a) Use Resolution to find the murderer. In other words, formalize the facts as a set of clauses, prove that there is a murderer, and extract his identity from the derivation."
 A: Let's call the hypothesis that Arthur is Victor's murderer, A. Likewise, that Bertram is the murderer, B, and that it's Carleton, C.
The one-of three condition is (a bit ugly):
A | B | C , ~(A & B), ~(A & C), ~(B & C)
Re-stated as clauses:
A | B | C , ~A | ~B, ~A | ~C, ~B | ~C
A sentence stated by some actor X can be false if X is the murderer, so all statements are to be extended by X | sentence to express that possibility.
Arthur says that Bertram was the victim’s friend (let's call that BF):
A | BF
Arthur says that Carleton hated the victim (let's call that CH):
A | CH
Bertram says that he was out of town (let's call being in place BP):
B | ~BP
We know that someone out of town can't be the murderer:
~BP -> ~B (clause BP | ~B)
Bertram says that he didn’t even know the guy (not V's friend):
B | ~BF
Carleton says that he saw Arthur and Bertram with the victim just before the murder (Arthur in place: AP):
C | AP
C | BP
~AP -> ~A (clause AP | ~A)
So, we have:
A | B | C  (1)
~A | ~B    (2)
~A | ~C    (3)
~B | ~C    (4)
A | BF     (5)
A | CH     (6)
B | ~BP    (7)
BP | ~B    (8)
B | ~BF    (9)
C | AP     (10)
C | BP     (11)
AP | ~A    (12)

Let's do some forward resolutions (did it by hand, hopefully without mistakes):
A | B      (13 = 5+9)
B | C      (14 = 7+11)
A | ~C     (15 = 13+4)
~C         (16 = 15+3)
C | ~A     (17 = 14+2)
~A         (18 = 17+3)
B          (19 = 13+18)

So, it's Bertram.
A: Let's call them A, B, C & V. If we can assume that there can only be a maximum of one liar, all we have to do is look for conflicting stories. In this case we see A and B have conflicting stories (A says B was V's friend, and B says he didn't know V), meaning one of them is lying. We can also see that B and C have conflicting stories (B says he was out of town and C says he saw them together), meaning again the same thing. Knowing that B conflicts with both A and C, we can deduce that either only B is telling the truth, or only B is lying. And since we know there can only be one liar, we know that A and C can't both be lying. So logically B has to be the murderer.
