類似性に基づく一般化知識の獲得と推論

基于相似性的广义知识的获取和推理

• 批准号: 04229217
• 负责人: 原尾 政輝
• 金额: $ 1.22万
• 依托单位: Kyushu Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 1992
• 资助国家: 日本
• 起止时间: 1992 至 1993
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-04229217/
• 关键词: 型理論; 知識表現; 概念階層; 抽象化階層; 一般化知識; 高階単一化; 類推; 類推証明

平成4年度は,次の具体的課題を設定して研究を進めた.(1)型の概念に基づく知識の類似性の定義.(2)類似性に基づく一般化知識の獲得,(3)類推システムの開発.まず,(1)については,型理論に基づいて高階論理言語を設計し,その言語を用いて知識のデータ構造,型階層,知識のモジュール構造などの知識表現を定義した.そして,同じ型の要素は似ているとの観点から,概念階層,抽象化階層の考えを新たに導入して知識間の類似性を定義し,代数的(束論的)意味論を展開した.次の(2)については,類似の知識集合を表す知識を一般化知識と呼び,概念階層や変数化(抽象化)による一般化知識の性質を性質を考察した.特に,対象とする知識を1階の論理式で表した場合の一般化知識を2階の論理式(これをスキーマとよぶ)として抽象化するための性質を明かにした.そして,高階単一化の手法を用いて,一般化知識を構成するアルゴリズムを設計した.特に,類推証明システムのための,類似証明を特性化するスキーマの導出法について幾つかの新しい結果を得た.(3)の課題については,一般化知識を用いた類推システムを設計し,高階単一化に基づく手続きを与えた.またこの方式を,LK論理系の論理式の証明問題に応用し,類推に基づくLK類推証明システムを開発した.開発には言語Isabelleを用しており.スキーマ28個と誘導問題10個を持ち,初級の証明問題は解けるシステムとなっている.

Heisei 4 years ago, the second time specific topics were set and research was advanced. (1)The definition of similarity of basic knowledge in the concept of type. (2)(3) the development of analogy system. In this paper, the author discusses the following: (1) The basic theory of type, the design of high-level logic speech, the use of speech, the structure of knowledge, the hierarchy of type, the structure of knowledge, and the definition of knowledge representation. The concept hierarchy, the abstract hierarchy, the introduction of new concepts, the definition of similarities between knowledge, the development of algebraic (bundle theory) implication theory. Second, similar knowledge sets represent generalized knowledge, conceptual hierarchies, digitization (abstraction), properties of generalized knowledge. In particular, the first order of knowledge is expressed in terms of generalized knowledge, and the second order of knowledge is expressed in terms of abstract knowledge. In this paper, the author discusses the design of high-level unified methods and the structure of generalized knowledge. In particular, analogical proof of the existence of a problem, similar proof of characterization of the problem of derivation of a problem of a problem (3)The topic is to use generic knowledge, analogy, design, high-level simplification, basic knowledge, and design. In this way,LK logic system logic formula proof problem is used, analogy is based on LK analogy proof system is developed. Isabelle's name is Isabelle. There are 28 induced problems and 10 persistent problems.

项目成果

M.Harao: "Analogical Reasoning For Natural Deduction Theorem Proving" Int.Workshop on Automated Reasoning(国際自動推論ワークショップ). Proceeding. 220-228 (1992)

M.Harao：“自然演绎定理证明的类比推理”自动推理研讨会220-228（1992）。

中川 祥子,原尾 政輝: "類推によるLK定理証明" 電子情報処理学会,コンピュテーション研究会. COMP92-36. 63-70 (1992)

Shoko Nakakawa，Masateru Harao：“通过类比证明 LK 定理”，IEICE，计算研究组 63-70 (1992)。

M.Harao: "LK Theorem proving By Analogy" 環太平洋人工知能国際会議(PRICAI'92). Proceeding. 714-720 (1992)

M.Harao：“类比证明 LK 定理”环太平洋国际人工智能会议（PRICAI92）（1992 年）。