書き換え帰納法に基づく帰納的定理の決定可能性

摘要

等式論理において，自然数やリストなどのデータ構造上で成立する等式を帰納的定理とよぶ．与えられた等式が等式論理の帰納的定理であるか否かは一般に決定不能であるが，いくつかの部分クラスに対する決定手続きが知られている．FalkeとKapur (2006)が与えた決定手続きは書き換え帰納法に基づく．一方，外山(2002)は，帰納的定理判定問題を2つの抽象リダクションシステムの等価性判定問題としてとらえることで，書き換え帰納法が帰納的定理の決定手続きとなるための十分条件を示した．しかし，この両者が保証している決定可能な帰納的定理のクラス間には包含関係がない．そこで，本論文ではこれら2つのアプローチを組み合わせることにより，従来保証されていた決定可能な帰納的定理のクラスを拡張する．