| 研究概要 |
本研究の主な成果は次の2項目である.
証明補完をまず,融合原理(resolution princeple)による矛盾の導出を用いた残余仮説の生成と一般化として定式化した.仮説生成が必要な状況では,与えられた事実は背景知識から帰結されないので,背景知識と事実の否定とが矛盾することはない.そこで,事実の否定と背景知識との基礎代入例(ground instance)の連言からブール代数によって恒偽な部分を除去して得られた詮理式を残余,その否定を残余仮説(residue hypothesis)とよぶ.残余仮説の一般化は融合原理の逆操作として定式化した.そして,アブダクションのための仮説生成規則や,帰納推論における底法(逆伴意法)や飽和法という推論現則が,残余仮説の導出とその一般化に様々な制限を与えたものであることを示すことができた.しかも,従来の仮説発見手法では仮説として単一の節しか生成できなかったが,残余仮説の導出を用いれば複数の節からなる仮説を同時に生成することができる.
次に,連結証明法(The Connection Method)を用いた証明補完を考察した.その結果;古典論理の範囲内で残余仮説を生成しているにも関わらず,与えられた事実と背景知識,残余仮説間の関係は,適切さの論理(relevant logic)の証明であることを明らかにした.適切さの論理では,前提となる論理式を全て利用することで帰結が証明される.この成果は,残余仮説に事実と背景知識を総動員してはじめて証明が完成していることを示している.仮説を生成する根拠はデータと背景知識しかないのであるから,仮説が事実の説明以上の能力を有しないという性質が,適切さの論理と結びつくのは自然な結果である.さらに,仮説発見には,複数個生成される仮説の中から適切な仮説を選択するという問題が常に付随するが,その基準として証明補完に証明の性質を用いた仮説の選択基準があることを示していることが明らかになった.
|
