文献

J-GLOBAL ID：201502213439604770   整理番号：15A0327275

項書き換えシステムの変換を利用した帰納的定理自動証明

Automated Inductive Theorem Proving using Transformations of Term Rewriting Systems

著者 (4件)： 佐藤洸一 (東北大学電気通信研究所) ,  菊池健太郎 (東北大学電気通信研究所) ,  青戸等人 (東北大学電気通信研究所) ,  外山芳人 (東北大学電気通信研究所)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 32  号： 1  ページ： 1.179-1.193 (J-STAGE)  発行年： 2015年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 項書き換えシステム上の帰納的定理の自動証明手法として書き換え帰納法(Reddy, 1989)が提案されている.しかし,書き換え帰納法は末尾再帰による関数定義が含まれると有効に働かない場合が多い.一方,プログラムの自動検証を容易にすることを目的としたプログラム変換法として,文脈移動法および文脈分割法(Giesl, 2000)が提案されている.これらの手法は,末尾再帰プログラムを自動検証に適した単純再帰プログラムへと変換する.本論文では,項書き換えシステムに対する文脈移動法・文脈分割法の正当性を証明し,それらが書き換え帰納法による帰納的定理の証明に有効であることを明らかにする.(著者抄録)

シソーラス用語： *数理言語学 ,  *証明 ,  分割法
準シソーラス用語： プログラム自動検証 ,  プログラム変換法 ,  *定理自動証明 ,  文脈分割法

分類 (1件)： 数理言語学  (JB05000V)

タイトルに関連する用語 (2件)： 項書き換えシステム ,  定理自動証明