如何在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 here中的解决方案。 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 = 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.
    neighbor(Rice,Green).
    Genoa = Five.
    Spanish = Seven.
    right_neighbor(Marseille,Spanish).
    Hamburg = Red.
    neighbor(Seven, White).
    border(Corn).
    Black = Eight.
    neighbor(Corn,Rice).
    Hamburg = Six.

end_of_list.

另存为ships.in

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