有限区間制約を付加したモデル生成型定理証明系とその応用

情報処理学会 Web Site 参考文献14件

書誌事項

タイトル別名
  • ユウゲン クカン セイヤク オ フカ シタ モデル セイセイガタ テイリ ショウメイケイ ト ソノ オウヨウ
  • Model Generation Theorem Proving with Finite Interval Constraints and Its Application
  • 知識処理

この論文をさがす

抄録

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

Model Generation Theorem Proving (MGTP) is a class of de-duction procedures for first-order logic that were successfully used to solve hard combinatorial problems. For some applications the representation of models in MGTP and its extension CMGTP causes redundancy. Here we suggest to extend members of model candidates in such a way that a predicate p can have not only terms as arguments, but at certain places also subsets of totally ordered finite domains. The ensuing language and deduction system relies on constraints based on finite intervals in totally ordered sets and is called IV-MGTP. We show soundness/completeness of the procedure, and the experimental results that show considerable potential of the method.

収録刊行物

参考文献 (14)*注記

もっと見る

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ