プレスブルガ一文付き項書換え系における書換え帰納法について

摘要

手続き型プログラムを等価な制約付き項書換え系に変換してプログラム等価性を検証する手法の研究において，潜在帰納法と呼ばれる手法が制約付き項書換え系に対応するように拡張されている．しかし．潜在帰納法七同じく帰納的定理を証明する手法である書換え帰納法は制約付き項書換え系に対応するように拡張されていない．本論文では，制約付き項書換え系に対応するように書換え帰納法を拡張し，それに基づいた帰納的定理の定理自動証明法を提案する．また，制約をプレスブルガー文に限定した場合に，潜在帰納法よりも簡潔に証明できる例を紹介する．%A method for verifying equivalence between procedural programs has been proposed .where the implicit induction is extended to deal with constrained term rewriting systems. However, the rewriting induction, which is used for proving inductive theorems, has not been adapted to constrained systems yet. In this paper, we extend the rewriting induction for constrained term rewriting systems, and propose a procedure based on the method for proving constrained inductive theorems. In the case that constraints are Presburger formulas, we show an example of inductive theorems of which the proof by the procedure is simpler than by the method based on implicit induction.