A Model Generation Theorem Prover Handling Finite Interval Constraints

DOI IR (HANDLE) Web Site Open Access
  • Hähnle Reiner
    Department of Computing Science, Chalmers Technical University
  • Shirai Yasuyuki
    Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University : Graduate Student | Information Technologies Development Department, Mitsubishi Research Institute, Inc.
  • Hasegawa Ryuzo
    Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University

Bibliographic Information

Other Title
  • Model Generation Theorem Prover Handling Finite Interval Constraints

Search this article

Description

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 representation 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.

Journal

Keywords

Details 詳細情報について

Report a problem

Back to top