| 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
|
| Project Status |
Completed (Fiscal Year 1990)
|
| Budget Amount *help |
¥1,400,000 (Direct Cost: ¥1,400,000)
Fiscal Year 1990: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1989: ¥600,000 (Direct Cost: ¥600,000)
|
|---|
| 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.
|
