title: Expressing Einstein Puzzle as a Set of Closed Formulas in First Order Logic
body: <p>I am given the classic Einstein/Zebra puzzle in this form:</p>
  
  <p>Let us assume that there are five houses of different colors next to each other on the same road. In each house lives a man of a different nationality. Every man has his favorite drink, his favorite brand of cigarettes, and keeps pets of a particular kind. </p>
  
  <pre><code>The Englishman lives in the red house. 
  The Swede keeps dogs. 
  The Dane drinks tea. 
  The green house is just to the left of the white one. 
  The owner of the green house drinks coffee. 
  The Pall Mall smoker keeps birds. 
  The owner of the yellow house smokes Dunhills. 
  The man in the center house drinks milk. 
  The Norwegian lives in the first house. 
  The Blend smoker has a neighbor who keeps cats. 
  The man who smokes Blue Masters drinks bier. 
  The man who keeps horses lives next to the Dunhill smoker. 
  The German smokes Prince. 
  The Norwegian lives next to the blue house. 
  The Blend smoker has a neighbor who drinks water. 
  The question to be answered is: Who keeps fish?
  </code></pre>
  
  <p>The task is to express these statements as a set of closed formulas in first order logic, one for each of the statements, given the assumptions that the five persons in the puzzle are represented by englishman, swede, dane, norwegian, german, and keep(X,Y) means person X keeps pet Y. These will then later be converted to prolog.</p>
  
  <p>My question is if I'm going about converting the statements in the right way.  Right now, I have something like:</p>
  
  <pre><code>color(X, red) → lives(englishman, X)
  keep(swede, dog)
  drinks(dane, tea)
  color(X, red) ∧ color(Y, green) → leftof(X, Y)
  color(X, green) ∧ lives(Y, X) → drinks(Y, coffee)
  smokes(X, pallmall) → keep(X, birds)
  color(X, yellow) ∧ lives(Y, X) → smokes(Y, dunhills)
  </code></pre>
  
  <p>Is this correct, or should it be more like the other way I tried it:</p>
  
  <pre><code>house(X) ∧ color(X, red) → lives(englishman, X)
  dog(X) → keep(swede, X)
  tea(X) → drinks(dane, X)
  house(X) ∧ house(Y) ∧ color(X, green) ∧ color(Y, white) → leftof(X, Y)
  house(X) ∧ color(X, green) ∧ lives(Y, X) ∧ coffee(Z) → drinks(Y, Z)
  pallmalls(X) ∧ smokes(Y, X) ∧ birds(Z) → keep(Y, Z)
  house(X) ∧ color(X, yellow) ∧ lives(Y, X) ∧ dunhills(Z) → smokes(Y, Z)
  </code></pre>
  
  <p>I also attempted something like:</p>
  
  <pre><code>lives(englishman, redhouse)
  keep(swede, dogs)
  drinks(dane, tea)
  leftof(greenhouse, whitehouse)
  lives(X, greenhouse) → drinks(X, coffee)
  smokes(X, pallmall) → keep(X, birds)
  lives(X, yellowhouse) → smokes(X, dunhills)
  </code></pre>
  
  <p>I think the first one is most correct, but I'm not sure.  I'm also not sure how to represent something like center or neighbor in first order logic.  Are any of these close to being correct?</p>
  
  <p>EDIT: I've come up with a solution that I think is possibly correct.  I noticed that it said CLOSED formulas, so I did it in this way:</p>
  
  <pre><code>lives(englishman, red)
  keep(swede, dogs)
  drinks(dane, tea)
  leftof(green, white)
  ∃X lives(X, green) ∧ drinks(X, coffee)
  ∃X smokes(X, pallmalls) ∧ keep(X, birds)
  ∃X lives(X, yellow) ∧ smokes(X, dunhills)
  ∃X position(X, 3) ∧ drinks(X, milk)
  position(norwegian, 1)
  ∃X,Y smokes(X, blend) ∧ neighbor(X, Y) ∧ smokes(Y, dunhill)
  ∃X smokes(X, bluemasters) ∧ drinks(X, bier)
  ∃X,Y keep(X, horses) ∧ neighbor(X, Y) ∧ smoke(Y, dunhill)
  smokes(german, prince)
  ∃X neighbor(norwegian, X) ∧ lives(X, blue)
  ∃X,Y smokes(X, blends) ∧ neighbor(X,Y) ∧ drinks(Y, water)
  </code></pre>
  
  <p>Is this the correct way to go about it? Any help would be appreciated.</p>