モデル生成型定理証明システムによる制約充足問題の解決とその並列化

白井　康之  長谷川　隆三  

誌名
電子情報通信学会論文誌 D   Vol.J80-D2   No.1   pp.224-236
発行日: 1997/01/25
Online ISSN: 
DOI: 
Print ISSN: 0915-1923
論文種別: 論文
専門分野: 人工知能，自然言語処理，認知科学
キーワード: 
自動証明,  制約充足問題,  準群問題,  モデル生成法,  OR並列,  

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



あらまし: 
有限領域の制約充足問題を解くために開発した二つのシステム，CPとCMGTPについて述べる．例題として有限代数分野における準群の存在問題を扱う．CPは制約論理型言語（CLP）に基づいているが，既存のCLPでは処理できない負の制約伝搬処理をデータ構造を工夫することによって可能にしており，準群の存在問題に関しては，他のシステムに比べ卓越した結果を示した．また，CMGTPは，モデル生成型の定理証明システムMGTPに負情報に関する処理を加えたもので，準群の存在問題に関してはCPと同等の枝刈り能力をもつ．CMGTPは1階述語論理による汎用の記述形式をもち，一般の制約充足問題に対しても適用可能である．また，CMGTPの並列化方式について説明し，並列マシン上で実際に行った実験結果について紹介する．