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?

What i tried. I extracted several propositions from the definition:


*

*S: didn't kill C

*S: J knew C

*S: W disliked C

*J: didn't kill C

*J: J didn't know C

*J: out of town

*W: didn't kill C

*W: S with C

*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?
 A: 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.
A: 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.
A: 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)
A: 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
A: There is no real recipe for solving such puzzles, except that (in my experience) it is really important to focus on finding the simplest possible formalization, and then use the shape of the formulas as a guide to finding the solution.  (As another example, see https://math.stackexchange.com/a/619400/11994.)
$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\calcop}[2]{\\ #1 \quad & \quad \unicode{x201c}\text{#2}\unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}
\newcommand{\implies}{\Rightarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$In this case we will write $\;s,j,w\;$ for the three suspects, one is which is equal to $\;m\;$, the guilty man.  We write $\;T(x)\;$ for '$\;x\;$ always tells the truth', so if $\;x\;$ says "$\;P\;$" then we can represent that as $\;T(x) \implies P\;$.  Finally, it seems important to explicitly represent '$\;x\;$ knew Cooper', and we will represent this as $\;K(x)\;$.
Now we are given quite some information given explicitly, where $\;x\;$ represents any suspect:
\begin{align}
\tag a  T(x) & \;\implies\; x \not=m \\
\tag b  T(s) & \;\implies\; K(j) \land K(w) \\
\tag c  T(j) & \;\implies\; \lnot K(j) \\
\tag d  T(w) & \;\implies\; K(s) \land K(j) \land (s = m \lor j = m) \\
\tag e  T(x) & \lor x = m \\
\end{align}
And there is an implicit fact, viz. that the murderer knew his victim:
$$
\tag f  K(m)
$$
Now our goal is to find the $\;x\;$ for which $\;x = m\;$.

Looking at the shape of these formulas, we notice that $\;K(j)\;$ occurs multiple times.  As there seems no obvious way to do rewriting, let's try a case split.
If $\;K(j)\;$ is false, then the right hand sides of $\ref b$ and $\ref d$ are false, and therefore (by contraposition) also their left hand sides are false, so $\;\lnot T(s)\;$ and $\;\lnot T(w)\;$.  Therefore (by $\ref e$, which says that $\;\lnot T(x) \implies x=m\;$) both $\;s=m\;$ and $\;w=m\;$, which makes $\;s=w\;$, which is a contradiction to the distinctness of $\;s,j,w\;$.
Therefore $\;K(j)\;$ is true, and therefore (by $\ref c$ and contraposition) $\;\lnot T(j)\;$, and therefore (again by $\ref e$) $\;j=m\;$.

Note that we did not need to use $\ref a$ and $\ref f$, and we also ignored a large part of the right hand sides of $\ref b$ and $\ref d$.
Translating the above proof into words, we get something like this:

If Jones did not know Cooper, then both Smith ("Cooper was a friend of Jones") and Williams ("[I] saw [...] Jones with Cooper") lied, and therefore only Jones speaks the truth, contradicting the fact that at least the two innocents speak the truth.  Therefore Jones lied when he said that he did not know Cooper, and therefore he is not innocent: Jones is the guilty man.

However, if the answer is only presented in this way, then it is a kind of surprise for the reader-- and that should be avoided, as much as possible.  Therefore I prefer to use the shape of the formulas to construct the answer.
