大規模法令論理式ベースの解析

∀x[行為(x)∧防衛(x)→正当(x)]

防衛行為は罪にはあたらない．

∀x[行為(x)∧防衛(x)→ ¬罪(x)]

においては同じ概念を記述するのに否定記号を用いるかど うかに恣意性がある．本 研究で対象とする不具合には以下のようなものを含む．

1.論理的矛盾

2.反対語および両立不可能(incompatible)な概念などを含んだ広義の対立概念．

3.定義の循環．

まず論理的矛盾とは異なる対立概念の例として，ある物体xが同時にcarであり shipであることは不可能である．

∀x[car(x)∧ship(x)→ ⊥] carとshipは概念として両立不可能であることを，

car∧ship ⊥

のように宣言を行い，この二つが否定に準ずる対立関係であるとする．さらに ve-hicle(乗り物)がcar(車)とship(船)を下位範疇化しており，その共通集合は空 ⊥ であることを示すと，

⎧⎪

⎪⎪

⎪⎪

⎨

⎪⎪

⎪⎪

⎪⎩

vehicle carvehicle shipvehicle

⊥ car

⊥ ship

は概念階層上のラティス(束: lattice)をなす．ここでラティスとは元a,bに対して

ab(共通の最大下位概念)，ab(共通の最小上位概念)が一意に定まるような集

合をさし，

• aa=a, aa=a(べき等則)

• a(bc) = (ab)c, a(bc) = (ab)c(結合則)

• ab=ba, ab=ba (交換則)

• a(ab) =a, a(ab) =a(吸収則)

3.3. 大規模法令論理式ベースの解析 57 を充たす．さらに分配則，有界のもの

• a(bc) = (ab)(ac), a(bc) = (ab)(ac) (分配則)

• ⊥とが存在する．(有界(bounded)ラティス)

を有界分配ラティスという．ちなみに上記の構造に補元が存在するとブール代数 となる．

不具合検出を行うには，すべての規則を同時に起動させてみる必要がある．例 えば，

∀x[vehicle(x)→prohibied(x)]

∀x[vehicle(x)→admissible(x)]

という二つの規則に対して，それらを同時に起動する vehicle(x)という知識を人 工的に追加し，無矛盾検出を行うことができる．

{vehicle(x)} ∪

vehicle(x)→prohibited(x) vehicle(x)→admissible(x)

⊥ where

{prohibited(x)∧admissible(x)} ⊥.

ここでprohibitedとadmissibleが対立概念であれば，⊥を産出する．このような 人工的に加える知識をassumptive facts と呼ぶ．図3.2はこのようなassumptive

factsを一斉に加えて推論規則の対立を発見するためのアルゴ リズムである．図中，

assumptive factsはPfact0(a)およびPfact1(b)である．また，

P2(x,y) :- P3(x), P4(x) P1(x,y) :- P2(x,y) P0(x,y) :- P1(x,y) P5(x) :- P4(x) P6(x) :- P5(x)

など の規則を連鎖させたものである．ここに P0(x, y)∧P6(x)→ ⊥ であるとす ると，二つのassumptive factsからこれらの規則群が矛盾を含んでいることがわ かる．

さて，このようなアルゴ リズムを実装するにはいくつかの問題がある．まず as-sumptive facts全体の発見であるが，すべての規則をexhaustiveに検索し，その前 提部を集め，かつ重複を取り除くのに効率の良いアルゴ リズムが望まれる．また，

すべてのassumptive factsが同時に必要かというとそうでもない．

図3.2: Assumptive factsからの矛盾 Q(x) :- P1(x), P2(x).

-Q(x) :- P2(x), P3(x).

のような規則のペアに対してP₁(x)∧P₂(x)∧P₃(x)は確かにQ(x)∧ ¬Q(x)という 矛盾を起こす．しかしP₁(x)∧P₂(x)やP₂(x)∧P₃(x)が現実的に可能な組み合わ

せでもP1,P2,P3がすべて同時に成り立つような組み合わせは現実的でない可能性

がある．これらがオントロジーからの対立概念によってすべて発見されていれば よいが，そうとは限らない．したがって集められたassumptive factsの集合自身の 中に既に対立の概念が含まれていないかど うかを精査する必要がある．また先に 述べたように帰結部に‘or’を含むような構造を含め，すべての規則がホーン節と して不適当な形態をしている場合の式変形，あるいは連鎖を行わせるにあたって 引数の数を一致させる式変形など ，法推論とは本質的ではないところで恣意的な 操作を行う必要がある．図3.3は大規模知識ベースに対してassumptive factsを加 え，知識ベースに含まれる法令文を

• 安定な知識

• 半安定な知識(矛盾に寄与する可能性がある知識) に切り出し，極小の矛盾領域を同定するようすである．