有限区間制約を付加したモデル生成型定理証明系とその応用(<特集>次世代移動通信ネットワークとその応用)

概要

論文の詳細を見る
モデル生成型定理証明システムMGTP(Model Generation Theorem Prover)は,ボトムアップ計算に基づく一階述語論理の定理証明系である.MGTPならびにその拡張形であるCMGTPは,制約充足問題に対しても有効な手続きを提供し,有限代数分野において,未解決問題の証明に成功するなど,高効率な証明系であることが実証されているが,半面,整数によって表された区間などの順序付けられた有限領域に関する制約伝搬においては,その記述の汎用性ゆえに,冗長なモデルを生成することが明らかとなった.本論文においては,こうした問題点を解決するために,全順序有限領域の部分集合をモデル候補として許す新しい定理証明系の枠組みを提案し,その形式的意味論と演繹手続きを明らかにする.また,いくつかの問題に対して適用した実験結果を示し,その有用性を示す.最後に,この新しい枠組みと制約論理プログラミングや多値論理,非単調論理との関連についても言及する.
一般社団法人情報処理学会の論文
2002-12-15