Pythonで動作する命題論理モジュールを探しています。
ユーザーはテキスト領域に数式を入力する必要があります。次に、それが正しいかどうかを確認する必要があります。
入力テキストが正しいものと等しいかどうかを直接テストすることはできません。これは、順列などを考慮していないためです。
そのようなモジュールは存在しますか?
- 編集 -
これがプロジェクトのスクリーンショットです(デザインは完了していません):
これはあまり難しくありません。必要なのは、(a) 見つけるか、(b) 任意の命題を取り込んで真理値表を生成するユーティリティを作成することだけです。次に、2 つの命題について、2 つの真理値表を生成し、原子変数と最後の列がすべての行で一致することを確認するだけです。
これは、原子変数の数で O(2^n) であり、各命題に同じ数の原子変数が含まれていると仮定します。余分な無用な原子変数が含まれている可能性がある場合 (OR (b または NOT b) が a と同等であるなど)、同じ数の行を取得するために、より単純な命題の真理値表をパディングする必要があります。異なるアトミック変数の使用が許可されている場合、これはさらに困難になります。
P != NP と仮定すると、O(2^n) よりも優れた結果を出すことはできません。これは、多項式解が命題計算よりも一般的な充足可能性の問題を解決するためです。
真理値表を生成するには、(a) 原子変数の真理値の 2^n 順列すべてのリストを生成し (これを行う方法はたくさんあります)、(b) 真理値への任意の代入の命題を評価する必要があります。原子変数の。次に、両方のテーブルを作成して比較します。出来上がり!
私はちょうどこの質問に出くわしました。もう答えが必要かどうかはわかりませんが、SymPy を使用することをお勧めします。
あなたが提示した例のA、B、C ...は、命題ではなく、セットのようです。私が見る限り、これらのタイプのステートメントについても推論することはできますが、命題論理ほどではありません。
これらのステートメントを意味論的に比較するには (ここで必要なことです)、より複雑なロジックが必要になりますが、より簡単な方法は、すべてのステートメントをプレーン テキスト比較によって比較可能な形式に書き直すことです。つまり、可換性を無視することにより、このステートメント
(A ⋃ B) ⋂ C
この発言と同じだろう
C ⋂ (B ⋃ A)
これは完全な設定ではありませんが、認識されない同等のステートメントが存在する可能性があるため、論理的同等性を使用してこれを理解するプロセスははるかに困難になります。書き換えロジックを使用すると、ほとんど労力をかけずに、多かれ少なかれ目的を達成できます。基本的に必要なのは、交換可能な二項演算子を指定することだけです。同等のステートメントを書き換えるいくつかの方程式も追加されます。さらに追加する必要があるかもしれません... Maude http://maude.cs.uiuc.edu/で何かを書きました
mod VennDiagram is
--- sorts
sort Set .
sort Statement .
subsort Set < Statement .
--- propositional formulas
op a : -> Set .
op b : -> Set .
op c : -> Set .
op d : -> Set .
op e : -> Set .
op f : -> Set .
op g : -> Set .
op h : -> Set .
op i : -> Set .
op j : -> Set .
--- and so on ....
--- connectives
op ¬_ : Statement -> Statement .
op _∁ : Statement -> Statement . --- complement
op _∨_ : Statement Statement -> Statement [ comm ] .
op _∧_ : Statement Statement -> Statement [ comm ] .
op _↔_ : Statement Statement -> Statement [ comm ] .
op _→_ : Statement Statement -> Statement .
op _⋂_ : Statement Statement -> Statement [ comm ] .
op _⋃_ : Statement Statement -> Statement [ comm ] .
op _←_ : Statement Statement -> Statement .
vars S1 S2 S3 S4 : Statement . --- variables
--- simplify statemens through equivalence
eq S1 → S2 = ¬ S1 ∨ S2 .
eq S1 ↔ S2 = (S1 → S2) ∧ (S2 → S1) .
eq ¬ ¬ S1 = S1 .
eq S1 ← S2 = S2 → S1 .
eq ¬ ( S1 ∧ S2 ) = (¬ S1) ∨ (¬ S2) .
--- possibly other equivalences as well..
endm
--- check equality
reduce a ↔ b == (b → a) ∧ (a → b) .
reduce ¬ a ↔ ( a ∨ b ) == ¬ a ↔ ( b ∨ a ) .
reduce (a ⋃ b) ⋂ c == c ⋂ (b ⋃ a) .
--- what you need to do is to compare the right answer
--- with a student answer through a simple comparison..
--- reduce StudentAnswer == RightAnswer