Выражение головоломки Эйнштейна как набора замкнутых формул в логике первого порядка
Мне дана классическая головоломка Эйнштейна / Зебры в этой форме:
Предположим, что на одной и той же дороге есть пять домов разных цветов. В каждом доме живет мужчина разной национальности. У каждого мужчины есть его любимый напиток, его любимая марка сигарет, и он держит домашних животных определенного вида.
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?
Задача состоит в том, чтобы выразить эти утверждения в виде набора замкнутых формул в логике первого порядка, по одному для каждого из утверждений, учитывая предположения о том, что пять человек в загадке представлены англичанином, шведом, датчанином, норвежцем, немецком и (X,Y) означает, что человек X держит домашнее животное Y. Затем они будут преобразованы в пролог.
У меня вопрос, собираюсь ли я правильно преобразовать утверждения. Прямо сейчас у меня есть что-то вроде:
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)
Это правильно, или это должно быть больше похоже на другой способ, которым я пытался это сделать:
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)
Я также пытался что-то вроде:
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)
Я думаю, что первый является наиболее правильным, но я не уверен. Я также не уверен, как представить что-то вроде центра или соседа в логике первого порядка. Любые из них близки к тому, чтобы быть правильными?
РЕДАКТИРОВАТЬ: Я нашел решение, которое я думаю, возможно, правильно. Я заметил, что в нем указаны ЗАКРЫТЫЕ формулы, поэтому я сделал это следующим образом:
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)
Это правильный путь? Любая помощь будет оценена.