1990 Fiscal Year Final Research Report Summary
Higher Order Unification and Mechanization of Higher Order Theorem Proving System
| Project/Area Number |
01580020
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | Kyushu Institute of Technology |
|---|
Principal Investigator |
HARAO Masateru KIT, Fac. of CSSE Professor, 情報工学部, 教授 (00006272)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
FUJITA Kenetsu KIT, Fac. of CSSE Assistant, 情報工学部, 助手 (30228994)
|
|---|
| Project Period (FY) |
1989 – 1990
|
| Keywords | Higher order logic / lambda-calculus / Higher order unification / Theorem proving / Mechanization of Proving system / Logic language / Analogical reasoning / Inference mechanism |
|---|
| Research Abstract |
We have studied in this year by setting the following themes : (1) Formalization of higher order logic language based on lambda-logic, (2) Design of higher order unification algorithm for mechanizing theorem proving system, (3) Higher order inference system for knowledge processings.
For the theme (1), we designed a higher order program language by extending the Horn clause to a higher order case, and some results have been obtained. For the theme (2), a new class of higher order language in which the unification algorithm becomes computable has been made clear. Especially computational complexity of unification algorithm for 2nd order terms has been discussed precisely. For (3), we have demonstrated that a kind of analogical reasoning system can be realized in the framework of proposed higher order language, and it is ascertained that the proposed method is available for designing intelligent knowledge processing system.
|
