| 研究概要 |
項書き換えシステムに基づく帰納的定理の自動証明手法として提案されている潜在帰納法と書き換え帰納法の差異を解析するとともに、自動証明に有効な関連手法を研究し、以下の成果を得た。
1.書き換え帰納法の解析
潜在帰納法と書き換え帰納にそれぞれ反駁証明法を組み合わせると、両者の証明能力は理論的に一致することを明らかにするとともに、実際の証明システム上では両者の証明能力に差異が生ずる原因を解析した。その結果、前者はシステム全体の合流性を検証する必要があるため証明手続きが横型探索にもとづいているが、一方、後者は証明すべき対象のみに対する退行性の検証のみが必要とされるので証明手続きは縦型探索にもとづいており、それが実際の証明システム上での差異の生じた原因であることを明らかにした。
2.停止条件の解析
書き換えシステムにもとづく自動証明システムでは,リダクションの停止性を自動的に判定する手法の確立が重要である。依存対を拡張して、従来よりも強力な判定手法を確立した。
|
