Formalization of Higher Order Ingerence Mechanism Based on Type Theory and Its Application to Analogical Reasoning System

基于类型论的高阶推理机制形式化及其在类比推理系统中的应用

• 批准号: 04650320
• 负责人: HARAO Masateru
• 金额: $ 1.28万
• 依托单位: Kyushu Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1992
• 资助国家: 日本
• 起止时间: 1992 至 1993
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-04650320/
• 关键词: Type theory; Knowledge representation; Inference machanism; Intelligent software; analogical system; Higher order program language; Theorem proving; Logic program; 高階論理; 類推; 知識ベース; 自然演繹証明; ML

In this research project, I set the following concrete themes :(1)Developments on knowledge representation and inference systems based on type theory.(2)Design of higher order program language and its processing system.(3)Realization of analogical reasoning system based on higher order abstraction.For the first teme, I have developped a theoretical properties on the knowledge representation and inference mechamisms using the logical framework, which is a kind of type theory. Especially, by introducing the concept such that type = proposition = concept, I have characterized the hierarchical properties in knowledge structures. I have also demonstrated that theunification and generalization, inheritance can be realized clearry in this framework.For the second theme, I have designed a kind of higher order program language using ML language, in which the processing mechanism works under the type inference. I confirmed that a kind of higer order representation and the processing based on inheritance are able to be established.For the third theme, I have realized a analogical reasoning system by choosing the object to the LK theorem proving problem. The analogical reasoning system have the similar ability to the one of average college students.By this research project, I believe that I could developped a new approch based on type theory to the branch of intelligent software language.

在本研究计画中，我设定了以下几个具体的主题：（1）基于类型理论的知识表示与推理系统的发展。（2）高级程序语言及其处理系统的设计。（3）基于高阶抽象的类比推理系统的实现。第一部分，利用逻辑框架（一种类型理论）对知识表示和推理机制进行了理论上的研究。特别是通过引入类型=命题=概念的概念，刻画了知识结构的层次性。在此基础上，本文设计了一种基于ML语言的高阶程序设计语言，其处理机制是在类型推理的基础上进行的。证明了一种高阶表示和基于继承的处理是可以建立的。第三个主题是通过对LK定理证明问题的对象选择，实现了一个类比推理系统。类比推理系统具有与普通大学生相似的推理能力，通过本课题的研究，我相信我可以为智能软件语言的分支开拓一条基于类型理论的新途径。

项目成果

Sakurai, Wakizono, Harao: "Analogical Reasoning Based on Abstraction" Information Processing. Vol.34, No.5. 558-565 (1993)

Sakurai、Wakizono、Harao：“基于抽象的类比推理”信息处理。

原尾: "Analogical Reasoning for LK Theorem Proving" Proc.of Tnter.Workshop on Automated Reasoning. North Hdland. 265-274 (1993)

Harao：“LK 定理证明的类比推理”Proc.of Tnter.Workshop on Automated Reasoning 265-274 (1993)。

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

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

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

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

原尾,中川: "類似性に基づく一般化知識の獲得と推論" 人工知能学会全国大会(1993年度). 41-44 (1993)

Harao，Nakakawa：“基于相似性的广义知识的获取和推理”日本人工智能学会全国会议（1993）41-44（1993）。