問題タブ [unification]

対話式のセマンティクスを記述する述語の参照解決を実行する場合、オープン ワールドで作業するため、部分的な統合を許容できる必要があります。

たとえば、次のシナリオを考えてみましょう。

目の前に青い箱があります。id を使用して、この青いボックスを参照します3。

一連の述語box(x)^blue(x)は、既知の青いボックスに簡単に解決できます。このクエリを実行すると、返されます3

述語のセットはball(x)^yellow(x)何にも解決されません。これで問題ありません。

しかし、今考えball(x)^yellow(x)^box(y)^blue(y)^behind(x,y) てみてください。それは、青いボックスの後ろにある黄色いボールです。

黄色いボールについてはわかりませんが、青いボックスについては知っています! もちろん、既知のボックスの後ろにボールがなく、別のボックスについて話されていた可能性もあります。しかし、どのボックスについて話しているかはわかっていると確信しています。

私は、一連の命題を満たすバインディングの各セットの確率を計算する確率論的枠組みの中で作業しています。次に、参照解決プロセスは、最も可能性の高い統合子/バインディングのセットを返します。残念ながら、 を考慮すると、私のシステムは、 id のボックスの後ろにある黄色のボールを認識していないため、にバインドされるbehind(x,y)可能性を一掃します。3y3

述語の部分的な統合を行う方法はありますか?システムが、ステートメントの解決が最も可能性が高い、y/3 x/?つまり y が 3 にバインドされ、x のアイデンティティが不明であると判断するようにする方法はありますか?

私はまだ解決策を持っていないこの特定の問題を抱えています。関連するアルゴリズムが存在することを知っていれば役立つと思います。

私が探しているアルゴリズムは、関数によって返される目標を満たす引数を見つけるのに役立つアルゴリズムです。

たとえばa works for b、(a,b)

関数worksはブール値との関係を保証します

今、私は与えられています

これら 2 つのバインディングを true にしたい場合、この関数は true でなければなりません

今、私はそのようなことを達成するのに役立つ関数/アルゴリズムを書こうとしています"x" = b

バックトラックを考えていましたが、まだ実装方法がわかりません。誰かが私にヒントを提供していただければ幸いです。

補足として、関数型プログラミング パラダイムを使用して F# でアルゴリズムを実装しています。

次の理論があるとします。

それは単に真であると言いますが、これはもちろん正しいのですa(X)が、存在b(X)しないため真です (否定は有限の失敗として)。b(X)が存在せず、 が存在する場合にのみ存在するためc(X)、c(a)これは真であると言えます。しかし、なぜPrologが答えを提供しないのか疑問に思っていましたX = aか? たとえば、いくつかのセマンティクスを紹介します。

もちろん、クエリを実行するnoOrphan(michael)と、結果はtrueとnoOrphan(david)になります(の親falseを定義していないためdavid)。?michaeldavidnoOrphan/1

これはおそらく Prolog のバックトラッキング メカニズムの結果ですが、Prolog は、肯定的な方法 (0,2,4,...) の否定の深さ、または否定的な方法 (1,3) で検索しているかどうかを検証する状態を維持できます。 ,5,...) 深い否定。

この式のペアが与えられた場合、MGU を見つけることは可能ですか?

1. f(x,y)
2. f(y,x)

x/y の場合は可能だと言いたかったのですが、それが合法かどうかはわかりませんでした。あなたたちは何を言いますか？

ありがとう！

インスタンス化されていないリストで呼び出すmember(Item, List)と、Prolog は項目を含むリストを統合して返します。true/を返しfalse、統一しようとしないルールが必要です。そのような規則はありますか？

関数の理由を理解しようとしています

タイプを持っています

フィルターがブール型を返す関数を受け取る必要があり、fst がタプルの最初の要素を返すだけの場合、「フィルター fst」はどのように機能しますか?

誰でも私を説明できますか？ありがとう ;）