1

人間にとって明らかな非常に単純なステートメントを証明するために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つの可能性を書き留めることができます）. 追加の or ステートメントを追加して問題を修正するべきではありませんが、既存の証明を遮断するべきではありませんが、現在の解決策にはなりません。3. ステートメント (pattern(Dan, Girrafe) は事実上、不必要な可能性を切り捨てます (それなしでは、どのプログラムが正しい解を見つけます)。

私がprover9をうまく使っていないのか、単に私の問題（または古典的なブールステートメントでの表現）で何かを見落としているのか、私にはわかりません。何が間違っている可能性がありますか？

4

1 に答える 1

0

特定の動物は 1 枚の T シャツにのみ使用できるというステートメントを追加します: all x (pattern (Dan, x) -> (- pattern(Tom, x) & -pattern (Louise, x)))。

これは、これを推論したときの私たちの行動を捉えています。ダンにはキリンがいて、ルイーズにはラクダがいません。ルイーズもキリンを飼うことができないので、ルイーズはパンダを飼う必要があります。

これが追加されると、最初の一連のステートメントと問題からの情報が証明につながります。

制約の 2 番目の定式化が機能した (最初の定式化では機能しなかった) 理由は、オプションが少ないためです。解決は、ステートメントを接続法標準形に変更します。指定されたステートメントの形式は (A & B & C) | （A＆D＆E）。分配法則を適用すると、9 つの別個のステートメントが導き出されます。あ、あ | D、A | E、B | A、B | D、B | E、C | A、C | D、C | E. これらはそれぞれ 2 つの部分しかありません。-pattern(Louise, Camel) が導出されると、解決により、これらのステートメントの一部が単一のプリミティブに削減され、証明が完了します。

制約の最初の定式化にはより多くのオプションがあり、それを接続法正規形に変更すると、次のようなステートメントになります。パターン(ダン、パンダ) | pattern(ルイーズ、パンダ) | パターン (ルイーズ、キリン)。

% 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.
于 2016-10-18T04:16:24.147 に答える