Prover9 找不到正确的解决方案

Question

我尝试使用 prover9 来证明对人类来说显而易见的非常简单的陈述，但幸运的是我无法让它发挥作用。我有以下情况：

% Three boys - Dan, Louise and Tom have t-shirts in three diffrent colors
% (white, yellow and green) and with three different patterns: (giraffe, camel and
% panda). Dan has the t-shirt with giraffe, Louise has the yelow one and Tom has
% not the white t-shirt. The boy with the yellow one has not the one with camel
% pattern. Task:
% Represent exercise with classical boolean statements and using 
% resolution algorithm answer the question: "who has the t-shirt with the camel pattern?"

formulas(sos).
%      (pattern(Dan, Giraffe) & pattern(Louise, Panda) & pattern(Tom, Camel))
%    | (pattern(Dan, Giraffe) & pattern(Louise, Camel) & pattern(Tom, Panda))
%    | (pattern(Dan, Panda) & pattern(Louise,Giraffe) & pattern(Tom, Camel))
%    | (pattern(Dan, Panda) & pattern(Louise, Camel) & pattern(Tom, Giraffe))
%    | (pattern(Dan, Camel) & pattern(Louise, Panda) & pattern(Tom, Giraffe))
%    | (pattern(Dan, Camel) & pattern(Louise, Giraffe) & pattern(Tom, Panda)).
    % This does not works, unfortunately

      (pattern(Dan, Giraffe) & pattern(Louise, Panda) & pattern(Tom, Camel))
    | (pattern(Dan, Giraffe) & pattern(Louise, Camel) & pattern(Tom, Panda)).
    % This works

      (color(Dan, White) & color(Louise, Yellow) & color(Tom, Green))
    | (color(Dan, White) & color(Louise, Green) & color(Tom, Yellow))
    | (color(Dan, Yellow) & color(Louise,White) & color(Tom, Green))
    | (color(Dan, Yellow) & color(Louise, Green) & color(Tom, White))
    | (color(Dan, Green) & color(Louise, Yellow) & color(Tom, White))
    | (color(Dan, Green) & color(Louise, White) & color(Tom, Yellow)).

    pattern(Dan, Giraffe).
    color(Louise, Yellow).

    -color(Tom,White).
    all x (color(x,Yellow) -> -pattern(x,Camel)).
end_of_list.

formulas(goals).
    pattern(Tom,Camel). % Our solution
    % pattern(Louise, Panda).
end_of_list.

1. 和 2. 公式是写下没有约束的所有可能性 - 简单排列 3！ （即使我们知道 Dan​​ 有长颈鹿，我们也可以写下 2 种可能性）。它不应该修改添加额外的问题或语句不应该切断我们现有的证明，但是它在我当前的解决方案中。 3. statement (pattern(Dan, Girrafe) de facto 切断了不必要的可能性（没有哪个程序找到正确的解决方案）。

我不知道我是否使用了不好的 prover9 或者只是在我的问题中忽略了某些东西（或者它在经典布尔语句中的表示）。我会做错什么？

Answer 1

添加一个声明，说明特定动物只能出现在一件 T 恤上： 所有 x (pattern (Dan, x) -> (- pattern(Tom, x) & -pattern (Louise, x)))。

这反映了我们在推理时所做的事情：丹有长颈鹿，而路易丝没有骆驼。既然路易丝不能同时拥有长颈鹿，那么路易丝就必须拥有熊猫。

添加后，您的第一组陈述和问题中的信息将导致证明。

使用第二种约束公式（但不适用于第一种）的原因是选项较少。解析将语句更改为合取范式。给定语句的形式为 (A & B & C) | (A & D & E)。应用分配律导致 9 个独立的陈述： A |一个，一个 | D、A |乙，乙|甲，乙| D, B | E, C | A, C | D, C | E. 每一个都只有两个部分。一旦 -pattern(Louise, Camel) 被导出，解析可以将其中一些语句简化为单个原语并完成证明。

约束的第一个公式有更多选项 - 将其更改为合取范式会导致诸如 pattern(Dan,Giraffe) |图案(丹,熊猫) |图案(路易丝，熊猫) |模式（路易丝，长颈鹿）。

% Saved by Prover9-Mace4 Version 0.5, December 2007.

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9   assign(max_seconds, 60).
end_if.

if(Mace4).   % Options for Mace4   assign(max_seconds, 60). end_if.

formulas(assumptions).

% Three boys - Dan, Louise and Tom have t-shirts in three different colors 
% (white, yellow and green) and with three different patterns: (giraffe, camel and 
% panda). Dan has the t-shirt with giraffe, Louise has the yellow one and Tom has 
% not the white t-shirt. The boy with the yellow one has not the one with camel 
% pattern. Task: 
% Represent exercise with classical boolean statements and using  
% resolution algorithm answer the question: "who has the t-shirt with the camel pattern?" 

%formulas(sos).
     (pattern(Dan, Giraffe) & pattern(Louise, Panda) & pattern(Tom, Camel))
    | (pattern(Dan, Giraffe) & pattern(Louise, Camel) & pattern(Tom, Panda))
    | (pattern(Dan, Panda) & pattern(Louise,Giraffe) & pattern(Tom, Camel))
    | (pattern(Dan, Panda) & pattern(Louise, Camel) & pattern(Tom, Giraffe))
    | (pattern(Dan, Camel) & pattern(Louise, Panda) & pattern(Tom, Giraffe))
    | (pattern(Dan, Camel) & pattern(Louise, Giraffe) & pattern(Tom, Panda)).
    % The above now works

      (color(Dan, White) & color(Louise, Yellow) & color(Tom, Green))
    | (color(Dan, White) & color(Louise, Green) & color(Tom, Yellow))
    | (color(Dan, Yellow) & color(Louise,White) & color(Tom, Green))
    | (color(Dan, Yellow) & color(Louise, Green) & color(Tom, White))
    | (color(Dan, Green) & color(Louise, Yellow) & color(Tom, White))
    | (color(Dan, Green) & color(Louise, White) & color(Tom, Yellow)).

    pattern(Dan, Giraffe).
    color(Louise, Yellow).

    -color(Tom,White).
    all x (color(x,Yellow) -> -pattern(x,Camel)).

   % Dan has the giraffe and Louise does NOT have the camel; therefore Louise     
   % has the Panda (because Louise cannot also have the giraffe)    
   % A pattern on Dan's t-shirt cannot be on Tom's or Louise's t-shirt
    all x (pattern (Dan, x) -> (- pattern(Tom, x) & -pattern (Louise, x))).

end_of_list.

formulas(goals).

pattern(Tom, Camel).

end_of_list.