6

実行する C++ オープン ソース ライブラリ (またはオープン ソースの Unix ツール) を探しています。

式は、実行時に AST ツリー、文字列、またはその他の形式で作成できます。

方程式はほとんどが単純な代数であり、未知の関数に関するいくつかの仮定があります。ドメインは、整数演算になります (関連する問題はよく知られているため、浮動小数点の問題はありません。@hardmath にストレスを与えてくれてありがとう、私はそれが既知であると仮定しました)。

例: 入力には function が含まれphiており、それに関する仮定 (ほとんどの場合)phi(x,y)=phi(y,x)があり、 を解決しようとします。

equality_test( phi( (a+1)*(a+1) , a+b ) = phi( b+a, a*a + 2a + 1 )

ファジーまたは任意の等式テストである可能性があります-つまり、常に成功する必要はありません(方程式が等しい場合でも「false」を返す場合があります)。

phi関数に関する上記のような仮定をサポートすることに問題がある場合は、私はこれを処理できます。そのため、単純な線形代数方程式の等価テスターも同様に歓迎されます。

  • C/C++ プログラミング ライブラリまたは Unix ツールの推奨事項を教えてください。（オープンソース）
  • 可能であれば、そのような等価テストが特定のライブラリ/ツールでどのように見えるかの例を添付していただけますか?

PS そのような equality_test が (成功した場合) 2 つの与えられた方程式の間で同形性 (つまり、一種の「マッピング」) を返すことができれば、大歓迎です。しかし、そのような機能を持たないツールも大歓迎です。

PS「ファジーテスター」とは、ランダムな入力に対するテストではなく、2つの関数の「同形」を探すという点で、内部方程式ソルバーが「ファジー」になることを意味します-確かにこれを実装できますが、試してみますより精度の高いものを見つけるために。

PPSブルートフォース「すべての入力テスト」よりも優れたパフォーマンスソリューションが必要な理由は別の問題です。上記の方程式は、方程式内の変数間のマッピングを持たない、私の内部問題の単純化された形式です。つまり、私にはeq1=phi( (a+1)*(a+1) , a+b )とがありeq2=phi( l+k, k*k + 2k + 1 )、それと を見つけなければなりませa==kんb==l。しかし、このサブ問題は、「総当たり」アプローチ (このアプローチの漸近的な複雑さでさえ) で処理できます。変数がわずかしかない場合は、8 とします。そのため、可能なマッピングごとにこの equation_test を実行する必要があります。その仕事を丸ごとできるツールがあれば、とてもありがたいし、そのようなプロジェクトに貢献できます。しかし、私はそのような機能を必要としません。単にequation_test()で十分であり、残りを簡単に処理できます。

要約すると：

  • equality_test() は、私が解決しなければならない多くの下位問題の 1 つにすぎないため、計算の複雑さが重要になります。
  • 100% 信頼できる必要はありませんが、いくつかのランダムな入力と変数マッピングを使用して方程式をテストするだけでなく、可能性が高くなります:)。
  • 「はい」または「いいえ」の出力 (すべての追加情報は役立つかもしれませんが、将来的には、この段階で「はい」/「いいえ」が必要です)
4

4 に答える 4

5

あなたのトピックは、自動化された定理証明の 1 つであり、そのために多数のフリー/オープン ソース ソフトウェア パッケージが開発されています。これらの多くは証明の検証を目的としていますが、求めるのは証明の検索です。

方程式の抽象的なトピックを扱うことは、数学者が多様体と呼ぶ理論になります。これらの理論には、モデルの存在と規則性に関して優れた特性があります。

実数または他のシステムを具体的に扱う方程式を念頭に置いている可能性があります。これにより、証明が求められる理論にいくつかの公理が追加されます。

原理的に、論理ステートメントが理論で証明できるかどうかを判断するアルゴリズムが存在する場合、その理論はdecidableと呼ばれます。たとえば、Tarski が 1951 年に示したように、実閉体の理論は決定可能です。しかし、そのようなアルゴリズムの実際の実装は不足しており、おそらく不可能です。

設計と開発の指針となる、何かを学ぶ価値のあるいくつかのオープン ソース パッケージを次に示します。

Tac: 汎用的で適応可能な対話型定理証明器

Prover9: 一次および等式論理の自動定理証明器

E(定理)定理証明者

于 2011-08-11T13:18:05.983 に答える
3

逆ポーランド記法を使用すれば、かなり遠くまで到達できると思います。

  1. RPNを使用して方程式を書き出す

  2. 変換を適用して、すべての式を同じ形式にします。たとえば、* A + BC-> + * AB * AC（RPNはA *（B + C）-> A * B + A * Cに相当）、 ^ * BCA-> * ^ BA ^ CA（つまり、（B * C）^ A-> B ^ A * C ^ A）

  3. 対称二項演算子の引数を「ソート」して、「軽い」演算が片側に表示されるようにします（A * B + C-> C + A * Bなど）。

  4. 合計インデックスなどのダミー変数で問題が発生します。他に方法はないと思いますが、方程式の両側でそれらを一致させるすべての組み合わせを試してみてください。

一般的に、問題は非常に複雑です。

ただし、ハックを試すことはできます。最適化コンパイラ（C、Fortran）を使用し、方程式の両側をコンパイルして最適化されたマシンコードを作成し、出力を比較します。動作する場合と動作しない場合があります。

于 2011-08-11T11:33:36.350 に答える
3

ライブラリについてはわかりませんが、方程式の入力のランダムなセットを生成し、比較する必要がある両方の方程式にそれを代入することで、自分でそれを行うのはどうですか. かなりの量のランダム データを生成すると、これによりほぼ正しい結果が得られます。

編集： http://www.wolframalpha.com/を試すこともできます

と

 (x+1)*(y+1) equals x+y+xy+2

と

 (x+1)*(y+1) equals x+y+xy+1
于 2011-08-11T11:10:29.910 に答える
1

オープンソース (GPL) プロジェクトMaximaには、 Wolfram Alpha の equals ツールと同様のツールがあります。

(a+b+c)+(x+y)**2 equals (x**2+b+c+a+2*x*y+y**2)

is (equal())は、式を解決します:

(%i1) is(equal( (a+b+c)+(x+y)**2 , (x**2+b+c+a+2*x*y+y**2) ));
(%o1)                                true

この目的のために、2 つの方程式の差を単純化するために、有理単純化器 ratsimpを使用します。2 つの方程式の差が単純化されてゼロになると、すべての可能な値について等しいことがわかります。

(%i2) ratsimp( ((a+b+c)+(x+y)**2) - ((x**2+b+c+a+2*x*y+y**2)) );
(%o2)                                  0

この回答は、方向を示しているだけです（他の回答と同様）。似たようなことを知っていれば、それは C++ Unix プログラム - プログラミング ライブラリの一部として使用できますか? これに似た優れた C/C++ バインディング ツール。新しい回答を投稿してください。

于 2011-08-29T22:44:20.190 に答える