0

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

一个港口有5艘船：

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

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

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

4

2 回答 2

0

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

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

于 2015-01-19T18:23:35.103 回答
0 
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

于 2019-11-28T16:39:49.727 回答