Embedding Negation as Failure into a Model Generation Theorem Prover
Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa
In Proc. of CADE-11, Lecture Notes in Artificial Intelligence, 607,
pp. 400--415, Springer, 1992.
この方法によれば、失敗による否定ならびに古典的否定(強い否定)
を含む disjunctive logic program を MGTP 上に実現することができ、
生成されるモデルが安定モデルであることが保証されている。
以下に、この方式の概略を示す。
失敗による否定を含む問題節は以下のような形式からなる。
¬KL,L -> .
¬KL,KL -> .
L,L' -> .
KL,L' -> .
KL,KL' -> .
ここで、L は(正負)リテラル、L' は相補リテラルを表す。
これらはルールとして問題節中に記述することも
できるが、効率上好ましくないため、システムの内部で処理することが
望まれる。また、システム内部でこれらのスキームを保持することにより、
連言照合が行われた時点での単位反駁を早期に実現し、余分な計算を省くこと、
また、スキームを用いて選言に対する枝刈りを行うことによって、
冗長な枝の探索の枝刈りを行うことが可能になる。
これらの実現方法の詳しい内容については、
推論の効率化技法
を参照されたい。
さて、こうして NAF を MGTP ルールに変換することができた。これを
問題節とすることにより、安定モデルを含むすべてのモデルが
MGTP により導出される。ただし、ここで注意べきは、生成されるモデルの
すべてが安定モデルではないことである。具体的には、
仮説のみから構成されるようなモデルも含まれる。そこで、導出されたモデルから
安定モデルのみを抽出するために、以下の T-condition と呼ばれる条件が
必要になる。
【T-Condition】任意のリテラルLに対して、KL ∈ S (Sはモデル)ならば A ∈ S であるとき、モデルSは T-Condition を満たすという。