如何在 Prover9 中为爱因斯坦的船谜题建模（一阶逻辑）答案

【问题标题】：How to model Einstein's ships puzzle in Prover9 (first order logic)如何在 Prover9 中为爱因斯坦的船谜题建模（一阶逻辑）
【发布时间】：2015-01-18 11:52:46
【问题描述】：

我需要在 Prover9 中为以下谜题建模

一个港口有5艘船：

希腊船六点出发，载着咖啡。

中间的船有一个黑色的烟囱。

英国船九点出发。

蓝色烟囱的法国船位于运送咖啡的船的左侧。

载可可的船的右侧是一艘前往马赛的船。

巴西船正驶向马尼拉。

载米的船旁边是一艘带绿色烟囱的船。

去热那亚的船五点出发。

西班牙船七点出发，在前往马赛的船的右侧。

带红色烟囱的船驶往汉堡。

七点出发的船旁边是一艘带白色烟囱的船。

边境的船载着玉米。

黑色烟囱的船八点出发。

运送玉米的船锚定在运送大米的船旁边。

去汉堡的船六点出发。

哪艘船开往塞得港？哪艘船运茶？

据我所知，prover9 接受一阶逻辑子句。但我真的不擅长将自然语言转换为 fol。有人可以告诉我如何以一阶逻辑对此进行建模，或许可以告诉我如何转换第一条语句？

【问题讨论】：

Port Said 是一个端口吗？ 15 个陈述中的任何一个都暗示了塞得港的存在在哪里？我们知道有船载茶吗？我的意思是……这里有更多信息吗……比如“有 5 艘船，一艘载茶、一艘玉米、一份大米、一份咖啡和一份可可”？我们是否有 5 艘船在 5 个不同的时间离开，5 艘船有 5 种不同的烟囱颜色，前往 5 个不同的港口？我们知道所有 5 个端口的名称吗？
这就是此类任务的本质......对于三个实体（旗帜、烟囱颜色、出发时间），15 个语句给出了五个值，但只有四个用于目的地和货运。这些缺失值在最后一个问题中给出……（您可以将最后一个问题写为 16。一艘船运茶，一艘船前往塞得港）……但这些陈述足以在矩阵中留下两个洞船只。

标签： theorem-proving first-order-logic zebra-puzzle

【解决方案1】：

我觉得这不是问题的完整陈述。

也就是说，我相信这个问题类似于 Larry Wos 提出的问题，然后在 OTTER here 中提出了解决方案。 OTTER 和 Prover9 确实存在一些差异，但也有许多相似之处，所以这可能会有所帮助，同时查看 Prover9 的手册。

【讨论】：

【解决方案2】：

set(arithmetic).  % For the "right neighbor", "left neighbour"... relations.
assign(domain_size, 5).  % The five ships are {0, 1, 2, 3, 4}.

list(distinct).      % Objects in each list are distinct.
   [Greek, English, French, Brazilian, Spanish].        % nationalities are distinct
   [Black, Blue, Green, Red, White].          % exteriors are distinct
   [Nine, Five, Seven, Eight, Six].        % leaves at distinct hour
   [Hamburg, Genoa, Marseille, Manila, Port_Said].   % destination is distinct
   [Tea, Coffee, Cocoa, Rice, Corn].  % cargo is distinct
end_of_list.

formulas(assumptions). 
   % Definitions of "right_neighbor"...
   right_neighbor(x, y) <-> x < y.
   left_neighbor(x, y) <-> x > y.
   middle(x) <-> x = 2.
   border(x) <-> x = 0 | x = 4.
   neighbors(x, y) <-> right_neighbor(x, y) | left_neighbor(x, y). 

    Greek = Six.
    Greek = Coffee.
    middle(Black).  
    English = Nine.
    French = Blue.
    left_neighbor(Coffee, French).
    right_neighbor(Cocoa, Marseille).
    Brazilian = Manila.
    neighbors(Rice, Green).
    Genoa = Five.
    Spanish = Seven.
    right_neighbor(Marseille, Spanish).
    Hamburg = Red.
    neighbors(Seven, White).
    border(Corn).
    Black = Eight.
    neighbors(Corn, Rice).
    Hamburg = Six.

end_of_list.

另存为ships.in

用这个命令运行它：mace4 -c -f ships.in | interpformat

【讨论】：