如何在Prover9中模拟爱因斯坦的飞船谜题(一阶逻辑)

Question

我需要在Prover9中对下面的谜题进行建模

一个港口有5艘船：

1. 希腊船六点出发，载着咖啡。
2. 中间的船有一个黑色的烟囱。
3. 英国船九点出发。
4. 蓝色烟囱的法国船在一艘载有咖啡的船的左侧。
5. 运载可可的船的右边是一艘前往马赛的船。
6. 这艘巴西船正驶向马尼拉。
7. 在运送大米的船旁边是一艘绿色烟囱的船。
8. 一艘前往热那亚的船五点出发。
9. 西班牙船七点出发，在前往马赛的船的右侧。
10. 带有红色烟囱的船前往汉堡。
11. 七点出发的船旁边是一艘白色烟囱的船。
12. 边境上的船载有玉米。
13. 黑色烟囱的船在八点离开。
运送
14. 玉米的船停泊在运送大米的船旁边。
15. 开往汉堡的船六点出发。

哪艘船去塞得港？哪艘船载茶？

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

Answer 1

我觉得

这不是问题的完整陈述。

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

Answer 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