項書き換えシステムの変換を利用した帰納的定理自動証明 Automated Inductive Theorem Proving using Transformations of Term Rewriting Systems

この論文にアクセスする

著者

抄録

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

Rewriting induction (Reddy, 1989) is proposed as an automated theorem proving method on term rewriting systems. In general, rewriting induction does not work well for the term rewriting systems with tail recursion. On the other hand, context moving and splitting (Giesl, 2000) are proposed as program transformation techniques intended to facilitate automated verification for functional programs. These techniques transform tail recursive programs into simple recursive programs suitable for automated verification. In this paper, we prove that the correctness of these techniques for term rewriting systems, and show that the combination of rewriting induction and these techniques are useful in proving inductive theorems on term rewriting systems with tail recursion.

収録刊行物

  • コンピュータ ソフトウェア

    コンピュータ ソフトウェア 32(1), 1_179-1_193, 2015

    Japan Society for Software Science and Technology

各種コード

  • NII論文ID(NAID)
    130004892317
  • 本文言語コード
    JPN
  • ISSN
    0289-6540
  • データ提供元
    J-STAGE 
ページトップへ