Formalization of Higher Order Ingerence Mechanism Based on Type Theory and Its Application to Analogical Reasoning System
Project/Area Number |
04650320
|
Research Category |
Grant-in-Aid for General Scientific Research (C)
|
Allocation Type | Single-year Grants |
Research Field |
情報工学
|
Research Institution | Kyushu Institute of Technology |
Principal Investigator |
HARAO Masateru (1993) Kyushu Institute of Technology Professor, 情報工学部, 教授 (44266272)
原尾 政輝 (1992) 九州工業大学, 情報工学部, 教授 (00006272)
|
Project Period (FY) |
1992 – 1993
|
Project Status |
Completed (Fiscal Year 1993)
|
Budget Amount *help |
¥2,000,000 (Direct Cost: ¥2,000,000)
Fiscal Year 1993: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1992: ¥1,300,000 (Direct Cost: ¥1,300,000)
|
Keywords | Type theory / Knowledge representation / Inference machanism / Intelligent software / analogical system / Higher order program language / Theorem proving / Logic program / 高階論理 / 類推 / 知識ベース / 自然演繹証明 / ML |
Research Abstract |
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.
|
Report
(3 results)
Research Products
(25 results)