抽象モデル生成による不要節の削除

梅田 眞由美  越村 三幸  長谷川 隆三  

誌名
電子情報通信学会論文誌 D   Vol.J89-D   No.10   pp.2288-2295
発行日: 2006/10/01
Online ISSN: 1881-0225
DOI: 
Print ISSN: 1880-4535
論文種別: 論文
専門分野: 人工知能,認知科学
キーワード: 
定理証明,  節の抽象化,  節集合の前処理,  モデル生成,  

本文: PDF(221.6KB)
>>論文を購入


あらまし: 
自動定理証明(Automated Theorem Proving:ATP)システムに与える問題は節標準形(Clause Normal Form:CNF)という節集合の形式に変換されるのが一般的である.本論文では節集合の抽象化手法を提案する.そして,これにより得られる抽象節集合のエルブランモデルによって,もとの節集合の充足可能性判定には不要な節が判別できることを示す.与える問題の節集合からあらかじめ不要な節を削除しておくのは,ATPシステムの効率化に有効であると考えられる.ATPシステムのベンチマーク集TPTPに収められている5600題余りのCNF形式の問題に本手法を適用したところ,1割を超える問題で不要節を削除することができた.また,本手法が最新のATPシステムの性能向上にも寄与することを確かめた.