I am trying to formalize "Einstein's riddle" in predicate logic to practice.
A thief has stolen a rare fish and is hiding in his house. The street has five contiguous houses. Each house has exactly one of each of the following properties:
The Nationality of the owner (N)
The beverage that the owner drinks (B)
The colour of the House's walls (H)
The brand of cigarette smoked (S)
The animal dwelling there (A)
Note that $A_5$, the fish, isn't listed in the clues for obvious reasons.
Is this a reasonable/correct formalization of the problem? If not, why not? Whether or not it's correct, how can it be improved?
Rule 1: Each house/house owner has exactly one of each type of property (e.g. Only one nationality). There are five of each properties and each one is assigned to a house. $$ \forall P \in \lbrace N,B,H,S,A \rbrace \space \forall i \in \lbrace 1,2,3,4,5 \rbrace \space \exists x (P_i(x) \land \forall y \Rightarrow y=x) $$ Rule 2: Iff a house $x$ is directly to the left of house $y$, then house $x$ cannot be the 5th house and house $y$ must be one more than $x$ $$ \forall x \forall y \space T(x, y) \iff x \in \lbrace 1,2,3,4 \rbrace \space \land y = x+1 $$
Clue 1: The Brit lives in the house with the red walls. $$ \exists x \space N_1(x) \land H_1(x) $$
Clue 2: The Swede has a dog. $$ \exists x \space N_2(x) \land A_1(x) $$
Clue 3: The Dane drinks tea. $$ \exists x \space N_3(x) \land B_1(x) $$
Clue 4: The green house is directly to the left of the white house. $$ \exists x \exists y \space H_2(x) \land H_3(y) \land T(x,y) $$
Clue 5: The owner of the green house drinks coffee $$ \exists x \space H_2(x) \land B_2(x) $$
Clue 6: The bird owner smokes Pall Mall $$ \exists x \space S_1(x) \land A_2(x) $$
Clue 7: The owner of the yellow house smokes Dunhill $$ \exists x \space S_2(x) \land H_5(x) $$
Clue 8: The man living in the centre (3rd) house drinks milk. $$ B_4(3) $$
Clue 9: The Norwegian lives in the 1st house. $$ N_4(1) $$
Clue 10: The cat owner lives next to the man who smokes Blends. $$ \exists x \exists y \space A_3(x) \land S_3(y) \land \lnot (T(x,y) \iff T(y,x)) $$
Clue 11: The horse owner lives next to the man who smokes Dunhill. $$ \exists x \exists y \space A_4(x) \land S_2(y) \land \lnot (T(x,y) \iff T(y,x)) $$
Clue 12: The man who smokes Blue master drinks root beer. $$ \exists x \space S_4(x) \land B_5(x) $$
Clue 13: The German smokes Prince. $$ \exists x \space N_5(x) \land S_5(x) $$
Clue 14: The Norwegian lives next to the blue house. $$ \exists x \exists y \space N_4(x) \land H_4(y) \land \lnot (T(x,y) \iff T(y,x)) $$
Clue 15: The man who smokes Blends lives next to the man who drinks water. $$ \exists x \exists y \space S_3(x) \land B_3(y) \land \lnot (T(x,y) \iff T(y,x)) $$