＜紀要論文＞A Model Generation Theorem Prover Handling Finite Interval Constraints

作成者 作成者名 所属機関 所属機関名 Department of Computing Science, Chalmers Technical University 作成者名 所属機関 所属機関名 Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University : Graduate Student | Information Technologies Development Department, Mitsubishi Research Institute, Inc. 九州大学大学院システム情報科学研究科知能システム学専攻 : 大学院生 | (株)三菱総合研究所情報技術研究センター 作成者名 所属機関 所属機関名 Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University 九州大学大学院システム情報科学研究科知能システム学専攻 英語 九州大学大学院システム情報科学研究院 Faculty of Information Science and Electrical Engineering, Kyushu University 2000-09-26 5 2 167 172 Version of Record open access https://doi.org/10.15017/1515680 https://portal.isee.kyushu-u.ac.jp/ https://portal.isee.kyushu-u.ac.jp/ https://portal.isee.kyushu-u.ac.jp/ 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.続きを見る

本文ファイル

p167 pdf 682 KB 133

詳細

PISSN 1342-3819 2188-0891 AN10569524 1515680 査読有 Theorem proving Model generation Constraint propagation Interval/Extraval representation Extended interpretation 2015.05.18 2020.10.26