2

GNU Prolog で書かれたトートロジー チェッカーのオープンソース実装を探しています (SWI-Prolog の実装も受け入れられますが、GNU Prolog が推奨されます)。

次のようなクエリでプログラム入力をフィードしたいと思います。

A and (B or C) iff (A or B) and (A or C).

また

3^2 * (X + 2) == (9 * X) + 18.

もちろん、表記は次のように異なる場合があります。

(3 power 2) mul (X plus 2) equals (9 mul X) plus 18.

結果として私が期待するのは、「はい/いいえ」、「等しい/異なる」、「見つかった証明/証明を見つけることができなかった」などのブール値の答えです。

ftp://ftp.cs.yorku.ca/pub/peter/SVT/GNU/で GNU-Prolog のトートロジー チェッカーを見つけましたが、ライセンスが添付されておらず、Gnu Prolog 算術制約と算術機能を適用する方法の手掛かりがありません論理モデルだけを算術で拡張するため。

  • 他の同様のソルバーはありますか?
  • モデルを拡張するために算術機能を使用する方法の例。

ありがとう、グレッグ。

PS 算術によると、部分的なサポートを探しています - 提案されたソリューションが古典的なロジックを適切に処理して開く場合、単純なヒューリスティック (gnu-prolog 整数関数の例も歓迎) を使用して手動でコーディングできるいくつかの基本的なケースのみを処理したい-ソースコードは拡張するのに適しています:)。

PPS @larsmansが指摘したように、ゲーデルの不完全性定理によれば、 「すべての」式を証明する方法はありません。そのため、Gnu Prolog プログラムを探しているので、与えられた公理と規則のセットから証明できるものを探しています。そのような公理と規則のセットの例を探しています ;) もちろん、チェッカーは失敗する可能性があります-「いくつかの」ケースで動作することを期待しています:)。- 一方、ゲーデルの完全性定理があります ;)。

4

3 に答える 3

3

Prolog で拡張可能な定理証明器が必要な場合は、 leanCOPが主な代表であるリーン定理証明器のファミリを確認してください。555 バイトの Prolog で古典的な一次ロジックを処理します。

バージョン 1.0 は次のプログラムです。

prove(M,I) :- append(Q,[C|R],M), \+member(-_,C),
 append(Q,R,S), prove([!],[[-!|C]|S],[],I).
prove([],_,_,_).
prove([L|C],M,P,I) :- (-N=L; -L=N) -> (member(N,P);
 append(Q,[D|R],M), copy_term(D,E), append(A,[N|B],E),
 append(A,B,F), (D==E -> append(R,Q,S); length(P,K), K<I,
 append(R,[D|Q],S)), prove(F,S,[L|P],I)), prove(C,M,P,I).

leanCOP Web サイトには、より多くの機能を備えた、より読みやすいバージョンがあります。等価性と算術演算を自分で実装する必要があります。

于 2011-08-15T14:42:06.263 に答える
1

問題に制約ロジックプログラミングを使用できます。等式は直接結果を与えます (GNU Prolog の例):

?- X*X #= 4.
X = 2

不等式の場合、通常、制約が設定された後にインスタンス化を生成するようにシステムに要求する必要があります。これは通常、ラベル付けディレクティブ (GNU Prolog の例) を介して行われます。

?- 27 * (X + 2) #\= (9 * X) + 18.
X = _#22(0..14913080)
?- 27 * (X + 2) #\= (9 * X) + 18, fd_labeling(X).
X = 0 ? ;
X = 1 ? ;
X = 2 ? ;
Etc..

どのプロローグがどの種類の CLP を持っているかを示すリストは、ここにあります。CLP マルチカラムを確認してください。

Prolog システムの概要、Ulrich Neumerkel

さよなら

于 2011-08-31T08:54:33.287 に答える
0

モルデハイのベンアリによるコンピューターサイエンスの数学的論理で、トートロジーチェッカーをいくつか見つけました。残念ながら、それらはブール論理をカバーしています。どのような利点がありますか、彼の実装はPrologにあり、自動証明、またはそのような方程式の解法（または自動検証）に関連するさまざまなアプローチを提示します。

于 2011-08-29T22:24:26.917 に答える