|
一般論理プログラムは2値安定モデルや3値安定モデルによって定義できる。一方、SLDNF導出は完備化されたプログラムに対する手続きとして採用されている。SLDNF導出が、アブダクティブ手続きの基礎として用いられたとき、それが2値安定モデルに関して健全かどうかが検討されたが、3値安定モデルに関して健全であることが証明された。
このプロジェクトでは、アブダクティブ手続きのための失敗による否定の一般化と3値論理におけるアブダクションの枠組を扱っている。
失敗による否定を適用するとき、安全な規則、すなわち、負のリテラルが基礎であることを要請する。しかし、より一般的なアブダクションの仮説を得るために、安全でない規則(Shepherdsonの規則)を採用した。失敗による否定を一般化することにより構成されたアブダクティブ手続きが、一般的な3値安定モデルに関して健全であることを示した。さらに、3値論理に基づくアブダクションブの枠組を構成した。そこでは、従来のものより一般的な制約が定式化されている。その一般的な制約により、各命題は仮説か、理論と仮説から導けるか、それ以外かに区別されねばならない。また、仮説でもなく、理論からも導けない命題であることを示す調整機能をもったアブダクティブ手続きが構成できる。さらに、この制約は、一般的な3値安定モデルとよく対応している。
成果を少し具体的に述べると、論理プログラムの意味論として、安定モデルを一般化し、変数を含む領域で定式化し、また、安全でないSLDNF導出の意味論を明確にした。これらの基礎の上に、変数を含む仮説を導けるアブダクティブ手続き(一般化された失敗による否定を適用)を検討し、さらに3値アブダクション枠組の構成に到った。
|
