制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序

摘要

定理自動証明では手続きが停止せずに暴走してしまうことがある．その暴走を避けるために，制約付き項書換えに対する定理自動証明の手続きが潜在帰納法と書換え帰納法それぞれに対して提案された。 一方，書換えが停止性を持つにもかかわらず，計算が進むにつれて項に含まれる書換え可能な項の大きさが増大していく場合がある．このような書換え系での定理自動証明において，書換え系の停止性を保存するように等式を方向付けして追加することは，経路順序を用いる手法では困難である．本稿では，引数切り落とし法を導入しながら，制約付き書換え系の停止性を保存する等式の方向付けに適した簡約化順序の条件を示す．制約付きTRSの潜在帰納法と書換え帰納法における定理証明での等式の方向付けにおいて，その条件を満たす簡約化順序が有効であることを示す．