n個の要素U
のセットとm個のプロパティのセットが与えられ、 P
Pの各要素は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
どういうわけか解析ツリーを「正規化」してから比較する必要があると思います。誰かがアプローチの概要を説明したり、アーキテクチャをスケッチしたりできますか?