Higher Order Unification and Mechanization of Higher Order Theorem Proving System

高阶定理证明系统的高阶统一与机械化

• 批准号: 01580020
• 负责人: HARAO Masateru
• 金额: $ 0.9万
• 依托单位: Kyushu Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1989
• 资助国家: 日本
• 起止时间: 1989 至 1990
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-01580020/
• 关键词: Higher order logic; lambda-calculus; Higher order unification; Theorem proving; Mechanization of Proving system; Logic language; Analogical reasoning; Inference mechanism; 型理論; マッチング; 計算の複雑さ; 導出原理; 人工知能

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.

今年我们通过设定以下主题进行了研究：（1）基于可达逻辑的高阶逻辑语言的形式化;（2）用于定理证明系统机械化的高阶统一算法的设计;（3）用于知识处理的高阶推理系统.针对主题（1），我们通过将Horn子句扩展到高阶情况，设计了一种高阶程序语言，并取得了一定的成果。对于主题（2），已经明确了一类新的高阶语言，其中统一算法变得可计算。特别是对二阶项的统一算法的计算复杂性进行了详细的讨论。对于（3），我们证明了一种类比推理系统可以在所提出的高阶语言的框架下实现，从而证明了所提出的方法对于设计智能知识处理系统是有效的。

项目成果

Harao: "Analogical Reasoning Based on Higher Order Unification" First International Conference on Algorithmic Learning Theory,. Proceeding. 151-163 (1990)

原尾：《基于高阶统一的类比推理》第一届国际算法学习理论会议，。

K.Fujita,A.Togashi,S.Noguchi: "A Canonical Translation from Higner Order Logic to Typed Lambda Calculus." 人工知能学会誌. Vol.5 No.6. 796-807 (1990)

K. Fujita、A. Togashi、S. Noguchi：“从高阶逻辑到类型化 Lambda 演算的规范翻译。”人工智能学会杂志第 5 卷第 796-807 期（1990 年）。

原尾,岩沼: "高階ユニフィケ-ションにおける可解なクラスと計算の複雑さ" LAシンポシウム,京都大学数理解研講究録. No.7.31. 37-48 (1990)

Harao，Iwanuma：“高阶统一中的可解类和计算复杂性”，京都大学数学理解研究论文集，No.7.31（1990）。

原尾,岩沼: "高階ユニフィケ-ションの計算複雑さ"

Harao，Iwanuma：“高阶统一的计算复杂性”

K.Iwanuma,M.Harao,S.Noguchi: "Reconsideration of Pointwise Circumscription,Transformation of Non‐Recursive Predicate Circumscription into First‐Order Sentences" International eonference on Info.Japan. 351-356 (1990)

K.Iwanuma、M.Harao、S.Noguchi：“点式限制的重新考虑，非递归谓词限制到一阶句子的转换”Info.Japan 国际会议 351-356 (1990)。