Automation of inductive theorem proving in equational logic with multi-context reasoning

多上下文推理方程逻辑中归纳定理证明的自动化

• 批准号: 22700021
• 负责人: SATO Haruhiko
• 金额: $ 0.83万
• 依托单位: Hokkaido University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2010
• 资助国家: 日本
• 起止时间: 2010 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22700021/
• 关键词: 定理自動証明; 項書換え系; 帰納的定理証明

We have studied on the efficient procedure and reasoning strategy for automating inductive theorem proving, which is an important technique for verifying correctness of software systems. First, we proposed a proof method with multi-context reasoning, which can perform inferences commonly appearing in some different reasoning strategies simultaneously. Second, we proposed a principle for generating correct lemmas which are often required in inductive theorem proving.

归纳定理自动证明是软件系统正确性验证的重要技术，本文研究了归纳定理自动证明的有效过程和推理策略。首先，我们提出了一个多上下文推理的证明方法，它可以同时执行在一些不同的推理策略中常见的推理。其次，我们提出了一个原则，以产生正确的引理，往往需要在归纳定理证明。

项目成果

書き換え帰納法における文脈探索の有効性について

论上下文搜索在重写归纳法中的有效性

• 发表时间: 2011
• 作者: Haruhiko Sato;Masahito Kurihara;上田圭祐，西村治道;佐藤晴彦
• 通讯作者: 佐藤晴彦

Multi-context rewriting induction with termination checkers

带有终止检查器的多上下文重写归纳

• 发表时间: 2010
• 期刊: IEICE Transactions on Information and Systems
• 影响因子: 0.7
• 作者: Haruhiko Sato;Masahito Kurihara
• 通讯作者: Masahito Kurihara

Optimizing Mkb Tt (system Description) ⋆

优化 Mkb Tt（系统描述）⋆

• 发表时间: 2010
• 作者: S. Winkler;Haruhiko Sato;A. Middeldorp;M. Kurihara
• 通讯作者: M. Kurihara