2016-09-24 3 views
1

私はちょうどプロローグを勉強しています。頭がおかしくなりません。Prolog Unification with not()

は私がa(v).次のプログラムに

value(v). 

a(X) :- not(value(X)). 

があるとしvalue(v)が正しい証明することができるよう、私にはfalseを与えます。

a(w)実際にはvalue(w)がないので、試してみても正しいことは証明できません。

私の理解では、a(X).を要求すると、value(X)が妥当性を失わせる可能性がある最初の可能な値が与えられます。 value(v)だけが正しいので、無限の可能性があります。

しかし、なぜPrologは回答を続けるのですかfalse?すべての

+1

あなたは***改ざん***をどのように表示するかによって、偽とは何ですか?何かが間違っていることをどのように証明しますか?それの一つの見方は、証明不可能なものは全て偽*であり、真実であるものすべてが証明できる(あなたには議論の余地がある)世界に住んでいると想像することができます。プロローグでは、 '\ +'演算子は失敗のセマンティクスとして否定をもって動作します。これは上で説明したものです。いくつかの手がかりを与えることを願っています。 – Limmen

+0

はい、偽を定義できないと定義した場合、Prologは正しいと証明できない例を提供して目標を達成できますか? – user3207838

+0

しかし、私は問題はPrologが常に**本当に**を作ることを探しているということです。この場合、エンジンを元に戻すのですか? – user3207838

答えて

2

まず、ISO述語(\+)/1not/1の代わりにを使用してください。

第二には、用語のdisequalityを示すために(\+)/1を使用しないでください:(\+)/1はプロローグで不完全であり、したがって、論理的に鳴りません。 ではなく、論理否定であるが、むしろ " 証明可能"を示している。あなたのケースでは

?- value(X).は成功し、それは証明可能なので、クエリはを成功させるインスタンスがあるが?- \+ value(X).は失敗します。

特に、?- \+ value(a).が成功するです。

は、だから我々は持っている:

 
?-  \+ value(V). 
false. 

しかしより具体的なクエリが成功します。

 
?- V = a, \+ value(V). 
V = a. 

これは明らかに私たちは純粋な関係に期待論理的性質に反します。 を参照してください。

dif/2を使用する、用語のdisequalityを意味します。 Prologシステムがdif/2をサポートしていない場合は、論理的に安全な近似値としてiso_dif/2を使用してください。詳細については、を参照してください。

+0

申し訳ありません、わかりました。ですから、私の望む機能を実現するためには、Prologは設計上不可能な、改善の余地のある例を考え出す必要があります。 基本的に、Prologでこれを実装することはできますが(おそらく望ましくないかもしれませんが)、私が言及した振舞いを得ることができますか?あるいは、私はいくつかの基本的な論理概念が欠けていますか? – user3207838

+0

あなたのケースでは、 'dif/2'やその他の制約を使って病気を表現することができます:' dif(X、v) 'は、' X'が** '**''と異なる**と言います。これは成功し、目標が保持されていない限り*残存ゴール*を残します。他のドメインの場合、類似の制約があります。例えば、 'X#\ = 3'は' X'が3とは異なる**整数**であると述べています。 – mat

1

Prologは「閉じた世界の仮定」の下で動作します–それは私達がそれについて言ったことを知っているだけです。特に、我々は何もwu、または他のものについて約それを言ったそれはどのように私たちにそれらを生成することができますか?そして、なぜwuの前に来なければならないのですか?

賢明唯一のものは(X, dif(X,v))を生成するかもしれないが、それは異なる問題、すなわち、への答えだろう「a(X)が証明可能にしますか?」、Prologが実際に応答しているのではなく、"a(X)は証明可能ですか?"

、あなたの認知負担を和らげるtrueからYesにあなたの頭の中でPrologのプロンプトの回答の名前を変更し、falseからNoにします。

Yesは、プロローグが「はい、私はそれを証明することができる」と言っています。No –「いいえ、私はそれを証明できませんでした」

に変更してください。\+not_provableとしてください。