導出法に基づく定理証明系のJavaによる実現手法について

摘要

導出法に基づく定理証明システムをJava言語で構築することを前提として、変数項の扱い方に相違を持つ二つのデータ構造（FVar/BVar方式とTermlist方式と呼ぶ）を提案し,それらの単一化の性能比較を行った。 実験の結果、単一化の性能においては、深い入れ子構造の項が存在するような場合を除いては、Termlist方式の方が速いとの結論を得た。 また、両データ構造を取り入れた定理証明システムを試作し、簡単なべンチマーク問題を解かせてみたところ、全体的に見てTermlist方式のデータ構造の方がより速い時間で証明が可能であるという結論が得られた。