Alice, Bob and Carl are each either liars (always lie), or truth-tellers (never tell a lie).

Alice says "Bob is a liar"

Bob says "Carl is a liar"

Carl says "Alice and Bob are both liars"

Who is telling the truth? (use propositional logic/resolution to answer this question).

Answer: Carl and Alice are liars. Bob is a truth-teller.

Derivation:

A is "Alice is a truth-teller"
B is "Bob is a truth-teller"
C is "Carl is a truth-teller"

----------------

Sentences:

Alice says Bob is a big fat liar: A <=> !B
Bob says Carl is a liar:  B <=> !C
Carl says both Alice and Bob are liars:  C <=> (!A ^ !B)

------------------

Conversion to CNF

A <=> !B  is
(A => !B) ^ (!B => A) is
(!A v !B) ^ (B v !A)   add these two facts to KB.

B <=> !C is
(B => !C) ^ (!C => B) is
(!B v !C) ^ (C v B)    add these two facts to KB.

C <=> (!A ^ !B) is
[(C => (!A ^ !B)] ^ [ (!A ^ !B) => C] is
[(!C v (!A ^ !B)] ^ [ !(!A ^ !B) v C] is
[(!C v !A) ^ (!C v !B) ]  ^ [A v B v C] add these three facts to KB

---------------------------------------------------

KB:

1)  !A v !B 
2)   A v  B
3)  !B v !C
4)   B v  C
5)  !C v  !A
6)  !C v !B
7)   A v  B  v C

---------------------------------------------------

Try to prove that Alice is a truth-teller.
Add rule to KB (negation of what we want to prove)

8) !A

---------------------------------------------------
Resolution:

combine 8 and 2 to produce B (new rule)

9) B

combine 9 and 3 to produce !C (new rule)

10) !C

any more applications of resolution will result in facts already 
in the KB, so there is no point in continuing. We can't prove that
Alice is a truth-teller. We can try to prove she is a liar.

We start over with the initial KB, and now add A (we are trying to
prove Alice is a liar, so we add the negation to the KB).

KB:

1)  !A v !B 
2)   A v  B
3)  !B v !C
4)   B v  C
5)  !C v  !A
6)  !C v !B
7)   A v  B  v C

---------------------------------------------------

8) A

combine 8 and 1 to get !B

9) !B

combine 9 and 4 to get C

10) C

combine 8 and 5 to get !C

11) !C

combine 10 and 11 to get nothing, this is a contradiction and proves
that by adding the rule A to our KB messes things up, so !A must be true.
Alice is a liar.

To find out about Bob and Carl, we add !A to the KB (this is now a
derived fact!) and see if we can prove something about B and C.

To Prove B: add !B and do resolution.

1)  !A v !B 
2)   A v  B
3)  !B v !C
4)   B v  C
5)  !C v  !A
6)  !C v !B
7)   A v  B  v C
8)  !A

9)  !B

combine 9 and 2 to produce A

10) A

combine 10 and 8 to produce null, therefore !B messes things up,
so we have proved B is true.

To prove Carl is a liar we can add C to the KB, which can
then be reduced to null proving Carl is a liar. Intuitively we
can see Carl is a liar since Bob says so, and we know B (Bob is
a truth teller).

Sample Problem:

• The members of a bridge club are Joe, Sally, Bill and Ellen.
• Joe is married to Sally.
• Bill is Ellen's Brother.
• The spouse of every married person in the club is also the club.
• The last meeting of the club was at Joe's house
• Was the last meeting at Sally's house?
• Is Ellen married?

Another problem. Given these facts:

• Steve only likes easy courses.
• CompSci courses are hard.
• All the courses in the math department are easy.
• MATH-301 is a math course.

Use resolution to answer the question, "What course would Steve like?"