课题基金 / 基金详情

Research on program transformation systems based on automated theorem proving

Research on program transformation systems based on automated theorem proving
基于自动化定理证明的程序转换系统研究
批准号：
19500003
负责人：
TOYAMA Yoshihito
金额：
$2.41万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2007
资助国家：
日本
项目状态：
已结题
起止时间：
2007 至 2009
来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19500003/
关键词：
プログラム理論プログラム変換情報基礎定理自動証明書き換えシステム書き換え帰納法融合変換変換パターン補題自動導入法

项目摘要

项目成果

TOYAMA Yoshihito的其他基金

相似基金

相关文献

中文摘要
翻译
项重写系统理论被广泛应用于自动定理证明和计算模型领域。本研究旨在开发基于术语重写理论的自动程序转换系统的基本理论和原型。具体成果包括程序转换模板的自动构造方法、高阶程序的新的终止性证明、重写归纳引理的自动生成方法、术语重写系统的自动合流证明器。
英文摘要
The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. This research aims to develop basic theories and prototypes for automated program transformation systems based on term rewriting theory. Concrete results include an automated construction method of program transformation templates, a new termination proof of higher-order programs, an automated lemma generation method for rewriting induction, an automated confluence prover of term rewriting systems.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
Termination proof of S-expression rewriting systems with recursive path relations
具有递归路径关系的S-表达式重写系统的终止证明
DOI： --
发表时间： 2008
期刊： LNCS Vol.5117
影响因子： --
作者： [Alvarado CG, Maruyama S, Cheng J, Ida-Yonemochi H, Kobayashi T, Yamazaki M, Takagi R, Saku T, Yoshihito Toyama]
通讯作者： Yoshihito Toyama
反証機能付き書き換え帰納法のための補題自動生成法
具有证伪功能的重写归纳法的自动引理生成方法
DOI： --
发表时间： 2009
期刊： コンピュータソフトウェア
影响因子： --
作者： [嶌津聡志, 青戸等人, 外山芳人]
通讯作者： 外山芳人
Argument Filterings and Usable Rules for Simply Typed Dependency Pairs
简单类型依赖对的参数过滤和可用规则
DOI： --
发表时间： 2007
期刊：
影响因子： --
作者： [T. Aoto, T. Yamada]
通讯作者： T. Yamada
Automatic Construction of Program Transformation Templates
程序转换模板的自动构建
DOI： --
发表时间： 2008
期刊： IPSJ Transactions on Programming 49
影响因子： --
作者： [Yuki Chiba, Takahito Aoto, Yoshihito Toyama]
通讯作者： Yoshihito Toyama
共 13 条
    Research on automated confluence proving for term rewriting systems
    • 批准号：
      22500002
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $2.33万
    • 财政年份：
      2010
    • 负责人：
      TOYAMA Yoshihito
    • 依托单位：
      Tohoku University
    Program verification method based on reduction approximations
    • 批准号：
      14580357
    • 项目类别：
      Grant-in-Aid for Scientific Research (C)
    • 资助金额：
      $1.79万
    • 财政年份：
      2002
    • 负责人：
      TOYAMA Yoshihito
    • 依托单位：
      Tohoku University
    Program verification based on higher order rewriting systems
    海外基金