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

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

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.