|
項書き換えシステムに基づく帰納的定理の自動証明手法として提案されている滞在帰納法と書き換え帰納法を解析し、以下の成果を得た。
1. 書き換え帰納法の定式化
書き換え帰納法を2つのシステムの等価性判定法として、抽象リダクションシステムの枠組で考察し、書き換え帰納法と滞在帰納法の本質的な差は、強正規性と弱正規性、および退行性と合流性にもとづいていることを明らかにした。したがって、両者の証明能力は異なることが示された。
2. 反駁証明法と組み合せた場合の比較
滞在帰納法と書き換え帰納法に、それぞれ反駁証明法を組み合わせると、両者の証明能力が一致することを明らかにした。したがって、実際の自動証明システムでは両者の能力に実質的な差は生じない。
3. 自動証明システムとの対応
上記の抽象的な枠組みをもちいて、実際に作成されている自動証明システムのメカニズムの解析を試みた。いくつかのシステムの解析を通して、本研究の定式化は、実際のシステム解析手法として有効であることを確認した。
|
