### Skapa referens, olika format (klipp och klistra)

**Harvard**

Hähnle, R., Hasegawa, R. och Shirai, Y. (2003) *Model Generation Theorem Proving with Finite Interval Constraints*.

** BibTeX **

@article{

Hähnle2003,

author={Hähnle, Reiner and Hasegawa, R. and Shirai, Y.},

title={Model Generation Theorem Proving with Finite Interval Constraints},

journal={Information Processing Society of Japan},

issn={0387-5806},

volume={43},

issue={12},

pages={4059-4067},

abstract={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 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.},

year={2003},

}

** RefWorks **

RT Journal Article

SR Print

ID 177259

A1 Hähnle, Reiner

A1 Hasegawa, R.

A1 Shirai, Y.

T1 Model Generation Theorem Proving with Finite Interval Constraints

YR 2003

JF Information Processing Society of Japan

SN 0387-5806

VO 43

IS 12

SP 4059

OP 4067

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

LA eng

OL 30