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

基于子句逻辑的知识发现系统基础理论构建及定理证明系统的实现

• 批准号: 10143201
• 负责人: 山本 章博
• 金额: $ 1.73万
• 依托单位: Hokkaido University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas (A)
• 财政年份: 1998
• 资助国家: 日本
• 起止时间: 1998 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10143201/
• 关键词: 帰納論理プログラミング; アブダクション; 底汎化法; 融合原理の完全性; 底節交差汎化法

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

The purpose of this study is: (1) to establish a unified theoretical basis for knowledge representation,(2) to demonstrate the high affinity of knowledge representation, and (3) to demonstrate the usefulness of knowledge representation. In recent years, attention has been paid to the development of logic theory (ILP), such as inverse association method, saturation method, repeated V algorithm, and the definition of common structure by research representatives. In this paper, we compare the soundness and completeness of the system. The results are as follows: (1)Horn logic is opposite, saturation method is opposite to Buntine's relative package,(2)Horn logic is opposite, base generalization method is opposite to repeated V algorithm, and the ability of generating theory is opposite,Plotkin's relative package is opposite to complete,(3) General node logic is opposite to base generalization method is opposite to Plotkin's relative package,(4) The method of generating theory is opposite to complete, and repeated V algorithm is opposite to complete.(4) The opposite meaning is opposite to the opposite meaning. The opposite meaning is opposite to the opposite meaning. The opposite meaning is opposite to the opposite meaning. The completeness theorem of the fusion principle guarantees the completeness of the fusion theory. The method of knowledge discovery and deduction is added to SOLDR derivation. For example, the number of background knowledge in ontology is limited to the number of definite nodes in the head set, and the number of finite parts in the base set is generated. In this case, the minimum generalization method is applied independently to each case. The method of cross difference generalization is proposed. This method is based on background knowledge and proof.

项目成果

Yamamoto, A.: "An Inference Method for the Complete Inverse of Relative Subsumption" New Generation Computing. 17・1. 99-117 (1999)

Yamamoto, A.：“相对包含的完全逆的推理方法”新一代计算 17・1（1999）。

Yamamoto, A.: "Revising the Logical Foundatons of Inductive Logic Programming Systems with Ground Reduced Program" New Generation Computing. 17・1. 119-127 (1999)

Yamamoto, A.：“用地面简化程序修改归纳逻辑编程系统的逻辑基础”，新一代计算，17・1。

Ito,K.and Yamamoto, A.: "Finding Hypotheses from Examples by Computing the Least Generalization of Bottom Clauses" Lecture Notes in Artificial Intelligence. 1532. 303-314 (1998)

Ito,K. 和 Yamamoto, A.：“通过计算底部子句的最小泛化从示例中查找假设”人工智能讲义。