節論理に基づく知識発見システムのための基礎理論の構成と定理証明系上での実現

点击翻译按钮获取中文摘要

本研究の目標は,(1)節論理を知識表現言語とする従来の様々な知識発見手法の統一的基盤となる理論を与え,(2)その基盤に基づいて融合(resolution)証明系に親和性の高い知識発見システムの構築技法を開発することで,様々な知識発見手法を駆使できる基盤システムを実現し,その実用性を実証することである.まず,帰納論理プログラミング(ILP)理論において近年注目されてきた仮説生成手法である逆伴意法,飽和法,反復V演算法,研究代表者が独自に開発した底汎化法に共通な構造を定義した.さらに,仮説生成システムの健全性と完全性を定義した上で,これらの手法を比較した.その結果,(1)Horn論理では,飽和法はBuntineの相対包摂に関して完全であること,(2)Horn論理では,底汎化法と反復V演算の仮説生成能力は等価であり,Plotkinの相対包摂に関して完全であること,(3)一般の節論理では底汎化法はPlotkinの相対包摂に関して完全であるが,反復V演算はそうではないこと,(4)逆伴意法は相対伴意に関しては完全ではなく,相対包摂に関しても完全ではないことを証明した.また,底汎化法はアブダクションと演鐸の合成であり,融合原理の完全性定理によってその完全性が保証されることを示した.知識発見システムを試作するにあたり,融合証明を演繹的に用いる方法として,SLD導出にスキップ操作とリダクション操作を追加したSOLDR導出を採用した.また,仮説と背景知識のクラスを本体の変数はすべて頭部に現ぶる確定節に限定することにより,底集合の有限部分集合で仮説の生成に十分なものを生成する.さらに,複数個の例に対しては,各例に対して底汎化法を独立に適用して仮説を生成し,それらの仮説の最小汎化を生成することとした.これを底節交差汎化法とよぶ.この方法で生成された仮説が背景知識Bに関して,すべての相対包摂することを証明した.