著者

藤平 光壮 岩沼 宏治

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会技術研究報告. AI, 人工知能と知識処理

巻号頁・発行日

vol.96, no.77, pp.17-24, 1996-05-24

---

逐次型探索において, 探索の順序は極めて重要である. PTTP型定理証明においては, ゴールの順序が探索の順序を決定する. ゴールの順序により探索空間の大きさが変わってしまう. 本研究では, 証明を開始する前に各リテラルの探索空間コストをある程度予測し, 探索空間が小さくなるようにリテラルの並び換えを行なう. 並び換えの方法をいくつか提案し, 実装, 性能評価実験, 他の証明器との比較実験を行なった.