4

n個の要素Uのセットとm個のプロパティのセットが与えられ、 PPの各要素はUからブール値までの関数を定義します。

フォームの2つの複合論理式(再帰的に定義された)が与えられた場合:

p1 : true iff p1(x) is true
e1 and e2 : means e1 and e2 are both true
e1 or e2 : means e1 and e2 are not both false
not e1 : true iff e1 is false
(e1) : true iff e1

これらの論理式は、式ステートメント(解析ツリー)に解析されます。

任意のp1、p2について:4つのセット(p1とp2)、(p1とp2ではない)、(p1とp2ではない)、(p1とp2ではない)すべてが空ではないと仮定します。

論理式L1がL2のサブセットであるかどうかを判別したいと思います。つまり、Uのすべての要素xについて、L1(x)が真の場合、L2(x)は真です。

したがって、たとえば:

is_subset(not not p1, p1) is true
is_subset(p1, p2) is false
is_subset(p1 and p2 and p3, (p1 and p2) or p3) is true

どういうわけか解析ツリーを「正規化」してから比較する必要があると思います。誰かがアプローチの概要を説明したり、アーキテクチャをスケッチしたりできますか?

4

3 に答える 3

1

オブジェクト(x)には何もしないので、真理値のすべての組み合わせが可能な命題論理が必要p1pnようです。

したがって、本質的には、命題論理で定理証明を実行する必要があります。

は、と同じis_subset(e1,e2)論理演算子に変換されます。これらが普遍的に成り立つかどうかを知るために、 DPLLなどの充足可能性チェックのアルゴリズムを使用して否定が満たされないかどうかをチェックできます。e1 implies e2not e1 or e2

これは単なる出発点であり、命題論理の定理を証明するための他の多くのオプションがあります。

于 2012-11-27T06:36:11.093 に答える
0

各式を選言標準形に変換して、一方が他方の接続句のサブセットを含んでいるかどうかを確認できます。このアプローチの複雑さは、言及されたpnの数の指数として増大します。

于 2012-11-25T23:56:39.320 に答える
0

インストラクターは基本的にQuine-McCluskeyアルゴリズムの実装を望んでいると思います。 他の答えが示すように、問題は-NP困難であるため、実行時間は非常に速く増加することに注意してください。

于 2012-11-26T00:04:27.443 に答える