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

在本研究项目中，我设定了以下具体主题：(1)基于类型论的知识表示和推理系统的发展。(2)高阶程序语言及其处理系统的设计。(3)基于高阶抽象的类比推理系统实现。对于第一个主题，我利用逻辑框架发展了一种关于知识表示和推理机制的理论性质，这是一种类型论。特别是通过引入类型=命题=概念的概念，刻画了知识结构的层次属性。在此框架下，可以清晰地实现统一、概括、继承。对于第二个主题，我使用ML语言设计了一种高阶程序语言，其中处理机制在类型推理下工作。我确认了一种高阶表示和基于继承的处理是可以建立的。对于第三个主题，我通过选择LK定理证明问题的对象实现了一个类比推理系统。类比推理系统具有与普通大学生相近的能力。通过这个研究项目，我相信我可以为智能软件语言的分支开发一种基于类型理论的新方法。

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.