Discovery and proof of inductive theorems with multi-context reasoning systems for algebraic software

使用代数软件的多上下文推理系统发现和证明归纳定理

• 批准号: 16K00090
• 负责人: Kurihara Masahito
• 金额: $ 3.08万
• 依托单位: Hokkaido University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2016
• 资助国家: 日本
• 起止时间: 2016-04-01 至 2019-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-16K00090/
• 关键词: 帰納的定理; 定理自動証明; 定理自動発見; 補題生成; 多重文脈型推論; 代数的ソフトウェア; 項書換え系; 帰納的定理自動証明; 書換え帰納法; 多重文脈推論; 帰納的定理証明; 補助定理; 定理発見; 発散鑑定; 仕様記述・検証

项目成果

Automated proof and discovery of inductive thorems with rewriting induction over multi-context reasoning systems: state-of-the-art technologies and perspectives

通过多上下文推理系统重写归纳来自动证明和发现归纳定理：最先进的技术和观点

• 发表时间: 2018
• 作者: Masahito Kurihara;Haruhiko Sato;ChengCheng Ji
• 通讯作者: ChengCheng Ji

On Usefulness of Syntactically Complex Lemmas in Theory Exploration for Inductive Theorems

论语法复杂引理在归纳定理理论探索中的作用

• 发表时间: 2018
• 作者: 十川雄司;青山裕介;黒岩丈瑠;久代紀之;Haruhiko Sato and Masahito Kurihara
• 通讯作者: Haruhiko Sato and Masahito Kurihara

Lazy Evaluation Schemes for Efficient Implementation of Multi-Context Algebraic Reasoning Systems

高效实现多上下文代数推理系统的惰性评估方案

• 发表时间: 2016
• 作者: Chengcheng Ji;Masahito Kurihara
• 通讯作者: Masahito Kurihara

Multi-Context Automated Lemma Generation for Term Rewriting Induction with Divergence Detection

通过发散检测进行术语重写归纳的多上下文自动引理生成

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

Discovering Inductive Theorems Using Rewriting Induction

使用重写归纳法发现归纳定理

• 发表时间: 2016
• 作者: Haruhiko Sato;Masahito Kurihara
• 通讯作者: Masahito Kurihara