Express logic puzzles with proposition calculus notation

I’m trying to solve a logic puzzle that goes like this:

The police have three suspects for the murder of Mr. Cooper: Mr. Smith, Mr. Jones, and Mr. Williams. Smith, Jones, and Williams each declare that they did not kill Cooper. Smith also states that Cooper was a friend of Jones and that Williams disliked him. Jones also states that he did not know Cooper and that he was out of town the day Cooper was killed. Williams also states that he saw both Smith and Jones with Cooper the day of the killing and that either Smith or Jones must have killed him. Can you determine who the murderer was if one of the three men is guilty, the two innocent men are telling the truth, but the statements of the guilty man may or may not be true?

When i was young, i used to solve such puzzles graphically, drawing vertices and arrows and excluding impossible cases. But now i want to do that formally. How can i express this puzzle definition using proposition calculus notation, inference and truth tables? Or, in other words, when you stumble upon a logical puzzle and you want to solve it formally, what is your algorithm?

1. S: didn't kill C
2. S: J knew C
3. S: W disliked C
4. J: didn't kill C
5. J: J didn't know C
6. J: out of town
7. W: didn't kill C
8. W: S with C
9. W: J with C

There are 3 groups of propositions, two of them are always true, the third may contain either true or false statements. Let be $A = 1 \land 2 \land 3$, $B = 4 \land 5 \land 6$, $C = 7 \land 8 \land 9$. Then from How to find the logical formula for a given truth table? by using truth tables and Karnaugh maps i deduct that the statement “some two of A, B, C are true” looks like $(A \land B \land \neg C) \lor (A \land \neg B \land C) \lor (\neg A \land B \land C)$. But wait, “may or may not be true” means that all statements might be true, not that at least one is false (hence the NAND is not appropriate here). So the sentence should be reformulated as “at least some two of A, B, C are true”. Am i going in the right direction?

Solution 1:

You can ignore statements 1,4, and 7 as they contain no information. Then since 2 and 5 are contradictory, one is false, so W is innocent and speaks the truth. Presumably, 9 contradicts 6 (though maybe C was also out of town), so J is the killer. How you formulate your propositional logic is key-does it represent that 2 and 5 contradict and that 6 and 9 contradict? This is often hard going from English to propositional calculus.

Solution 2:

I think there is no definitive answer on how to solve such puzzles. The main thing is to know propositional calculus well so that one is able to express a puzzle as formulas.

I can give one possible way how to formally solve such puzzles using automated tools, which I used on this one:

First I expressed the puzzle in the TPTP language, which is used by many automated theorem provers. (The TPTP language is for first order logic, but propositional logic is possible too, one simply doesn't use propositional variables):

% Basic syntax:
% Lines starting with % are comments.
% A formula is given by fof(name, type, formula) where 'name' identifies the formula,
% 'type' is either 'axiom' or 'conjecture' and 'formula' is a logic expression.
% Predicates start with lower case letters, and you can use propositional
% connectives: |, &, =>, <=, <=>, <~> (XOR), ~ (negation).

% The police have three suspects for the murder of Mr. Cooper: Mr. Smith, Mr. Jones, and Mr.

% Williams. Smith, Jones, and Williams each declare that they did not kill Cooper.

% Smith also states that Cooper was a friend of Jones and that Williams disliked him.

fof(smith, axiom, (~s => ( ~s & j_friend ) )).

% Jones also states that he did not know Cooper and that he was out of town the day Cooper was killed.

fof(jones, axiom, (~j => ( ~j & ~j_friend & j_out ) )).

% Williams also states that he saw both Smith and Jones with Cooper the day of the killing and that either Smith or Jones must have killed him.

fof(williams, axiom, (~w => ( ~w & ~j_out & ~s_out & ( s | j ) ) )).

% Can you determine who the murderer was if one of the three men is guilty,

% the two innocent men are telling the truth,

% but the statements of the guilty man may or may not be true?

fof(guilty, axiom, (s & ~j & ~w) | (~s & j & ~w) | (~s & ~j & w) ).

% Uncomment one of the following conjectures:
%fof(conj, conjecture, j).
%fof(conj, conjecture, w).
%fof(conj, conjecture, s).

Since we know that only innocent people tell the truth and the guilty one may lie, we formalize "Jones states ..." as ~j => .... This tells us that if Jones is innocent, the thing he says is true; if he's guilty, we have no information.

Then I run a theorem prover, which decides if the conjecture is provable from the axioms or not (propositional problems are always decidable, so it will always give an answer). I used E prover for that:

eprover -l 0 --tstp-format puzzle.p

and I get a result, either

# No proof found!
# SZS status CounterSatisfiable

or

# SZS status Theorem
# Proof found!

depending on if my conjecture was provable or not.

I hope it helps you at least a bit.

Solution 3:

Define

$S$ = Smith is the killer

$J$ = Jones is the killer

$W$ = Williams is the killer

$TS$ = Smith is telling the truth

$TJ$ = Jones is telling the truth

$TW$ = Williams is telling the truth

$A$ = Cooper was a friend of Jones

$B$ = Williams disliked Cooper

$C$ = Jones knew Cooper

D = Jones out of town

E = Smith seen with Cooper

G = Jones seen with Cooper

Assumptions

$S \vee J \vee W$

$\neg (S \wedge J)$

$\neg (S \wedge W)$

$\neg (J\wedge W)$

$\neg S \rightarrow TS$

$\neg J \rightarrow TJ$

$\neg W \rightarrow TW$

$A \rightarrow C$

$G \rightarrow C$

$D \rightarrow \neg J$

The Facts

$TS \rightarrow A$

$TS \rightarrow B$

$TJ \rightarrow \neg C$

$TJ \rightarrow D$

$TW \rightarrow E$

$TW \rightarrow G$

The Proof

Combining Assumptions and Facts, use a truth table (preferably automated) to show that $$((S \vee J \vee W) \wedge \neg (S \wedge J) ... \wedge (TW \rightarrow G)) \rightarrow J$$

is a tautology. (For a nice truth table generator, see http://mathdl.maa.org/images/upload_library/47/mcclung/index.html)

Solution 4:

Here is the short and simple answer:

S. says J. and C. were friends J. says J. and C. didn't know each other.

So one of them is lying. This means W. is telling the truth.

W. says he saw both S. and J. with C. that day. J. says he was out of town.

This means J. is the one who is lying. Therefore, he must be the murderer