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！ （即使我们知道丹有长颈鹿，我们可以写下2种可能性）。它不应该修改问题，增加额外的或声明不应该切断我们现有的证据，但它使我在当前的解决方案。 3.声明（模式（丹，Girrafe）事实上切断不必要的可能性（如果没有这些程序找到正确的解决方案）。

我不知道，我是否使用严重prover9或者只是忽略了一些在我的问题（或在其古典布尔语句中的表示）我可以做什么错？

Answer 1

添加一条声明，说一只特定的动物只能在一件T恤上： 全部x（图案（丹，x） - >（ - pattern（Tom，x）& -pattern（Louise，x）））。

这个捕获了我们在理由时做的事情：Dan has the长颈鹿和路易丝没有骆驼。由于路易丝不能拥有长颈鹿，路易丝必须拥有熊猫。

一旦添加了这些信息，您的第一组陈述和来自问题的信息将导致证明。

事情与约束的第二个表达式（但不是与第一个）的工作原因是有更少的选项。解决方案将语句更改为连接范式。给定的陈述是（A & B & C）| （A & D & E）。应用分配法导致9个单独的陈述：A | A，A | D，A | E，B | A，B | D，B | E，C | A，C | D，C | E.每一个只有两个部分。一旦模式化（路易斯，骆驼）派生决议可以将这些语句中的一些减少为单个原语并完成证明。

约束的第一个表达式具有更多的选项 - 并将其更改为连接的普通形式会导致语句如模式（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.