0

次のように2つの前提がある場合：

  1. a -> c (a は c を意味する)
  2. b -> c (b は c を意味する)

そして導き出された結論：

  1. a -> b (したがって、a は b を意味します)、

次に、結論が無効であることを示すことができます。理由は次のとおりです。

a -> c は、a が真で c が真の場合、ステートメント #1 で有効です。b -> c は、b が偽で c が真の場合、ステートメント #2 で有効です。これは、a が true で b が false の場合に a -> b につながり、ステートメント #3 と直接矛盾します。

または、前提が真であるが結論が偽である行を含む真理値表による証明ごとに:

真の前提と偽の結論を含む真理値表

私の質問は次のとおりです。「プロローグを使用して、ステートメント #1 と #2 の主張がステートメント #3 の結論と矛盾していることを示す方法はありますか? もしそうなら、そうするための明確で簡潔な方法は何ですか?」

4

2 に答える 2

2

制約を使用して、すでに非常に良い答えを出しています。

また、CLP(B) を使用して、前提から結論が導かれないことを示すために、少し異なる方法を示したいと思います。

主な違いは、前提ごとに個別の 制約を投稿し、前提から結論が導かれるかどうかを確認するために使用することです。sat/1taut/2

最初の前提は次のとおりです。

a→c

CLP(B) では、これを次のように表現できます。

sat(A =< C)

第 2 の前提、すなわち b → c は次のようになります。

sat(B =< C)

これらの前提から a → b が続く場合、次のtaut/2ように成功しT = 1ます。

?- sat(A =< C), sat(B =< C), taut(A =< B, T).
偽。

そうではないので、前提から結論が導かれないことがわかります。

CLP(B) に反例を示すように求めることができます。つまり、a → c と b → c の両方が成り立ち、a → b が成り立たない変数への真理値の代入です。

?- sat(A =< C), sat(B =< C), sat( ~ (A =< B))。
A = C、C = 1、
B = 0。

この場合に存在するユニークな反例を示すには、制約を投稿するだけで十分です。反例が一意でない場合は、次のようlabeling/1に、グラウンド インスタンスを生成するために使用できますlabeling([A,B,C])。

比較のために、たとえば次のように考えてください。

?- sat(A =< B), sat(B =< C), taut(A =< C, T).
T = 1、
sat(A=:=A*B),
sat(B=:=B*C)。

これは、a → b ∧ b → c から a → c が成り立つことを示しています。

于 2016-10-15T07:46:21.197 に答える
1

library(clpb)を使用できます ：

まず、式を変数 Expr に代入します。

Expr = ((A + ~C)*(B + ~C)+(~(A + ~B)).

ご了承ください：

  • 「+」は論理和を表します

  • 論理 AND の場合は「*」

  • '~' は論理 NOT ともA->B同等A+(~B)です。したがって、上記の式は、 と を使用して記述した場所と同等((A->C),(B->C))-> (A->C)です。'->'+,~','*

クエリを実行すると、次のようになります。

?-  use_module(library(clpb)).
true.
?- Expr=((A + ~C)*(B + ~C))+(~(A + ~B)),taut(Expr,T).
false.

述語taut /2は入力として clpb 式を取り、トートロジーの場合は T=1 を返し、式が満たされない場合は T=0 を返し、それ以外の場合は失敗します。したがって、上記のクエリが失敗したという事実は、Expr もトートロジーでもなく、満たすことができなかったことを意味します。つまり、満たすことができたということです。

また、クエリを実行することによって:

?- Expr=((A + ~C)*(B + ~C))+(~(A + ~B)),sat(Expr).
Expr = (A+ ~C)* (B+ ~C)+ ~ (A+ ~B),
sat(1#C#C*B),
sat(A=:=A).

Predicatesat/1は、ブール式が充足可能である場合に True を返し、次の場合に上記の Expression が充足可能であるという答えを返します。

sat(1#C#C*B),
sat(A=:=A).

where'#'はexclusive ORが満たされるときに式 (taut/2 から充足可能であることがわかります) が満たされることを意味します1#C#C*B。

ライブラリを使用しない別の解決策は次のとおりです。

truth(X):-member(X,[true,false]).

test_truth(A,B,C):-
  truth(A),
  truth(B),
  truth(C),
  ((A->C),(B->C)->(A->C)).

例：

?- test_truth(A,B,C).
A = B, B = C, C = true ;
false.

また、あなたのコメントから正しく理解できた場合、考えられるすべての解決策を収集するために、次のように書くことができます。

?- findall([A,B,C],test_truth(A,B,C),L).
L = [[true, true, true]].

これにより、リストのリストが得られます。ここで、内側のリストは[true,true,true]上記の例の形式を持ちます。これは、ソリューションがA=true,B=true,C=true存在し、上記の場合、ソリューションが 1 つしかないことを意味します。

すべての矛盾を見つけるには、次のように記述できます。

 truth(X):-member(X,[true,false]).

    test_truth(A,B,C):-
      truth(A),
      truth(B),
      truth(C),
    not( (\+ ((\+A; C),(\+B ; C)) ; (\+A ; B)) ).

最後の行は次のように書くこともできます:

not( ( (A->C;true),(B->C;true) ) -> (A->B;true) ;true ).

例：

  ?- findall([A,B,C],test_truth(A,B,C),L).
L = [[true, false, true]].
于 2016-10-15T07:04:08.060 に答える