1996 Fiscal Year Final Research Report Summary
STUDIES ON REASONING PRINCIPLE BASED ON LOGICAL FRAMEWORK THEORY AND ITS APPLICATION TO HEURISTIC REASONING SYSTEM
| Project/Area Number |
07680405
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | KYUSHU INSTITUTE OF TECHNOLOGY |
|---|
Principal Investigator |
HARAO Masateru Kyushu Institute of Technology, Professor, 情報工学部, 教授 (00006272)
|
|---|
| Project Period (FY) |
1995 – 1996
|
| Keywords | Logic / Type theory / Logical framework / Intelligent reasoning / Hypothetical reasoning / Analogical reasoning principle / Heuristic reasoning / Intelligent language |
|---|
| Research Abstract |
In 1995, I have researched by focussing on the studies on the reasoning prrinciple based on the logical framework theory and intelligent language construction for intelligent reasoning systems. In 1996, I have researched mainly on the following themes from the viewpoints of inplemention of the heuristic reasoning system using the results obtained until now.
(1) Studies on language for Artificial intelligence based on the logical framework theory : Using the logical framework theory, I have investigated problems such that knowledge and data representation method, and the theoretical properties of inheritance mechanism which is essential for efficient system construction. An experimental language has been implemented according to the obtained results on the SUN workstation.
(2) Automatic proof generation based on the type theory : The relations between the type inference system and the LK sequent calculus has been investigated, and the problems of higher order proof method and unification theory are also discussed. Further, a method of producing a proof automaticaliy using the formulas as types principle in the type theory has been proposed and is formulated in the grammatical form.
(3) Proof discovery system based on analogy : A system which reasons and discover a proof of the first order sequent calculus in the similar mannar to human beings is implemented using a general theorem proving language ISABELLE on the SUN work station.
It has been recognized that the approach based on the logical framework theory is useful to formalize the reasoning principle and intelligent language through this research. I am planning to extend this approch for AI further.
|
