CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Model Generation Theorem Proving with Finite Interval Constraints

Reiner Hähnle (Institutionen för datavetenskap) ; R. Hasegawa ; Y. Shirai
Information Processing Society of Japan (0387-5806). Vol. 43 (2003), 12, p. 4059-4067.
[Artikel, refereegranskad vetenskaplig]

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.



Denna post skapades 2013-05-23.
CPL Pubid: 177259

 

Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)

Ämnesområden

Data- och informationsvetenskap

Chalmers infrastruktur