完備化に基づく自動証明技術の研究

基于补全的自动证明技术研究

• 批准号: 11780204
• 负责人: 鈴木 太郎
• 金额: $ 1.34万
• 依托单位: Tohoku University (2000)Japan Advanced Institute of Science and Technology (1999)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1999
• 资助国家: 日本
• 起止时间: 1999 至 2000
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-11780204/
• 关键词: 定理自動証明; 完備化手続き; ナローイング; 関数論理型言語処理系; 高階ナローイング計算系; 自動証明

本研究の目的は,等式を用いた自動証明技術として広い応用範囲をもつ完備化と呼ばれる手続きの高速な実装技術を提案することである.本研究では,等式を解くための手続きであるナローイングと完備化手続きとの類似性に着目し,ナローイングに基づく関数論理型言語処理系の実装で提案されているコンパイル技術を完備化手続きに応用することで完備化手続きの高速化をはかることを目的とした.今年度は,前年度提案した完備化手続きを高速に実装するための等式のコンパイル技術を用いて,実際にUNIX環境上に完備化手続きを実装した.具体的には,コンパイルされた等式からの危険対の生成と,実行時での動的な等式コンパイルのための命令セットをもつ抽象機械を実装し,完備化手続きの中に組み込んだ.これにより従来のものに比べてある程度の高速化を図ることができたが,期待したほどの効果は得られなかった.これは等式を簡約化する部分が従来の完備化手続きと同様に実装されていたためであった.この問題点を解決するために,今年度は等式のコンパイルされた表現をデータとみなして簡約を行う方法について検討を行い,実装を試みた.また,高階の完備化の理論的研究と関連して,前年度につづいて高階ナローイングに関する理論的研究を行った.前年度で提案した高階ナローイング計算系を出発点とし,その計算系が生成する解の探索空間をさらに縮小できるいくつかの改良点を発見した.それらを組み合わせることで,いくつかの新たな高階ナローイング計算系を提案した.

The purpose of this study is to propose a new method for the automatic proof of equations. In this paper, we study the similarity between the solution of the equation and the completion of the algorithm, and propose the implementation of the basic number-related logical speech processing system. This year, the previous year's proposal to complete the manual, high-speed implementation of the equation and the use of technology, in fact, UNIX environment to complete the manual implementation The concrete equation is to generate the dangerous pair, and the dynamic equation is to execute the abstract mechanical design, complete the manual design. This is the first time I've ever seen a woman. The equation is simplified and the algorithm is completed. This problem is solved in this year's reverse equation. In the previous year, the research on the theory of high-order completeness was carried out. As the high-level NARO IE computing system proposed in the previous year was released, the exploration space for generating solutions in the computing system has been reduced and improvements have been announced. A new high-level computing system is proposed.

项目成果

M.Marin,: "Cooperative Constraint Functional Logic Programming"T.Katayama et al. (eds.), International Symposium on Principles of Software Evolution (ISPSE 2000). 214-220 (2000)

M.Marin，：“协作约束功能逻辑编程”T.Katayama 等人。

T.Suzuki: "Complete Selection Functions for Lazy Conditional Narrowing"Proc.of 5th Fuji International Symposium on Functional and Logic Programming, LNCS. (To Appear). (2001)

T.Suzuki：“Complete Selection Functions for Lazy Conditional Narrowing”Proc.of 第五届富士函数与逻辑编程国际研讨会，LNCS。

M.Marin,T.Ida and T.Suzuki: "On Reducing the Search Space of Higher-Order Lazy Narrowing"Proc.of 4th Fuji International Symposium on Functional and Logic Programming, LNCS 1722. 319-334 (1999)

M.Marin、T.Ida 和 T.Suzuki：“论减少高阶惰性窄化的搜索空间”Proc.of 第四届富士函数和逻辑编程国际研讨会，LNCS 1722. 319-334 (1999)

M.Marin,: "Higher-Order Lazy Narrowing Calculi in Perspective"Proc.of the Nineth International Workshop on Functional and Logic Programming,. 238-252 (2000)

M.Marin，：“高阶惰性窄化演算视角”第九届国际函数和逻辑编程研讨会论文集。

T.Suzuki: "An Efficient Implementation of Completion Procedure"International Workshop on Symbolic and Numeric Algorithms for Scientific Computing. 2-2 (1999)

T.Suzuki：“完成程序的有效实施”科学计算符号和数值算法国际研讨会。