完備化に基づく自動証明技術の研究
完備化に基づく自動証明技術の研究
基于补全的自动证明技术研究
批准号：
11780204
负责人：
鈴木 太郎
金额：
$1.34万
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1999
资助国家：
日本
项目状态：
已结题
起止时间：
1999 至 2000
中文摘要
翻译
本研究の目的は,等式を用いた自動証明技術として広い応用範囲をもつ完備化と呼ばれる手続きの高速な実装技術を提案することである.本研究では,等式を解くための手続きであるナローイングと完備化手続きとの類似性に着目し,ナローイングに基づく関数論理型言語処理系の実装で提案されているコンパイル技術を完備化手続きに応用することで完備化手続きの高速化をはかることを目的とした.今年度は,前年度提案した完備化手続きを高速に実装するための等式のコンパイル技術を用いて,実際にUNIX環境上に完備化手続きを実装した.具体的には,コンパイルされた等式からの危険対の生成と,実行時での動的な等式コンパイルのための命令セットをもつ抽象機械を実装し,完備化手続きの中に組み込んだ.これにより従来のものに比べてある程度の高速化を図ることができたが,期待したほどの効果は得られなかった.これは等式を簡約化する部分が従来の完備化手続きと同様に実装されていたためであった.この問題点を解決するために,今年度は等式のコンパイルされた表現をデータとみなして簡約を行う方法について検討を行い,実装を試みた.また,高階の完備化の理論的研究と関連して,前年度につづいて高階ナローイングに関する理論的研究を行った.前年度で提案した高階ナローイング計算系を出発点とし,その計算系が生成する解の探索空間をさらに縮小できるいくつかの改良点を発見した.それらを組み合わせることで,いくつかの新たな高階ナローイング計算系を提案した.
英文摘要
本研究の目的は,等式を用いた自動証明技術として広い応用範囲をもつ完備化と呼ばれる手続きの高速な実装技術を提案することである.本研究では,等式を解くための手続きであるナローイングと完備化手続きとの類似性に着目し,ナローイングに基づく関数論理型言語処理系の実装で提案されているコンパイル技術を完備化手続きに応用することで完備化手続きの高速化をはかることを目的とした.今年度は,前年度提案した完備化手続きを高速に実装するための等式のコンパイル技術を用いて,実際にUNIX環境上に完備化手続きを実装した.具体的には,コンパイルされた等式からの危険対の生成と,実行時での動的な等式コンパイルのための命令セットをもつ抽象機械を実装し,完備化手続きの中に組み込んだ.これにより従来のものに比べてある程度の高速化を図ることができたが,期待したほどの効果は得られなかった.これは等式を簡約化する部分が従来の完備化手続きと同様に実装されていたためであった.この問題点を解決するために,今年度は等式のコンパイルされた表現をデータとみなして簡約を行う方法について検討を行い,実装を試みた.また,高階の完備化の理論的研究と関連して,前年度につづいて高階ナローイングに関する理論的研究を行った.前年度で提案した高階ナローイング計算系を出発点とし,その計算系が生成する解の探索空間をさらに縮小できるいくつかの改良点を発見した.それらを組み合わせることで,いくつかの新たな高階ナローイング計算系を提案した.
期刊论文(10)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
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 等人。
M.Marin，：“协作约束功能逻辑编程”T.Katayama 等人。
DOI：
--
发表时间：
期刊：
影响因子：
--
作者：
[]
通讯作者：
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。
T.Suzuki：“Complete Selection Functions for Lazy Conditional Narrowing”Proc.of 第五届富士函数与逻辑编程国际研讨会，LNCS。
DOI：
--
发表时间：
期刊：
影响因子：
--
作者：
[]
通讯作者：
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、T.Ida 和 T.Suzuki：“论减少高阶惰性窄化的搜索空间”Proc.of 第四届富士函数和逻辑编程国际研讨会，LNCS 1722. 319-334 (1999)
DOI：
--
发表时间：
期刊：
影响因子：
--
作者：
[]
通讯作者：
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，：“高阶惰性窄化演算视角”第九届国际函数和逻辑编程研讨会论文集。
M.Marin，：“高阶惰性窄化演算视角”第九届国际函数和逻辑编程研讨会论文集。
DOI：
--
发表时间：
期刊：
影响因子：
--
作者：
[]
通讯作者：
T.Suzuki: "An Efficient Implementation of Completion Procedure"International Workshop on Symbolic and Numeric Algorithms for Scientific Computing. 2-2 (1999)
T.Suzuki：“完成程序的有效实施”科学计算符号和数值算法国际研讨会。
T.Suzuki：“完成程序的有效实施”科学计算符号和数值算法国际研讨会。
DOI：
--
发表时间：
期刊：
影响因子：
--
作者：
[]
通讯作者：
ＧＮＳＳ受信機とカメラの融合による新しい移動体測位手法の研究
-
批准号：12J06592
-
项目类别：Grant-in-Aid for JSPS Fellows
-
资助金额：$2.53万
-
财政年份：2012
-
负责人：鈴木 太郎
-
依托单位：
高精度GPS技術を用いた小型自律飛行ロボットによる情報収集手法の開発
-
批准号：09J02960
-
项目类别：Grant-in-Aid for JSPS Fellows
-
资助金额：$1.79万
-
财政年份：2009
-
负责人：鈴木 太郎
-
依托单位：
海外基金