<紀要論文>
A Model Generation Theorem Prover Handling Finite Interval Constraints

作成者
本文言語
出版者
発行日
収録物名
開始ページ
終了ページ
出版タイプ
アクセス権
JaLC DOI
関連DOI
関連URI
関連情報
概要 Model generation theorem proving (MGTP) is a class of deduction procedures for first-order logic that were successfully used to solve hard combinatorial problems. For some applications, the representa...tion of models in MGTP and its extension CMGTP is too redundant. In this paper, 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. It is related to constraint programming and many-valued logic, but differs significantly from either. We show soundness and completeness of IV-MGTP. First results with our implementation show considerable potential of the method.続きを見る

本文ファイル

pdf p167 pdf 682 KB 133  

詳細

PISSN
EISSN
NCID
レコードID
査読有無
主題
登録日 2015.05.18
更新日 2020.10.26

この資料を見た人はこんな資料も見ています