Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class

Pascal Fontaine 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The Bernays-Schönfinkel-Ramsey (BSR) class of formulas is the class of formulas that, when written in prenex normal form, have an quantifier prefix and do not contain any function symbols. This class is decidable. We show here that BSR theories can furthermore be combined with another disjoint decidable theory, so that we obtain a decision procedure for quantifier-free formulas in the combination of the BSR theory and another decidable theory. The classical Nelson-Oppen combination scheme requires theories to be stably-infinite, ensuring that, if a model is found for both theories in the combination, models agree on cardinalities and a global model can be built. We show that combinations with BSR theories can be much more permissive, even though BSR theories are not always stably-infinite. We state that it is possible to describe exactly all the (finite or infinite) cardinalities of the models of a given BSR theory. For the other theory, it is thus only required to be able to decide if there exists a model of a given cardinality. With this result, it is notably possible to use some set operators, operators on relations, orders -- any operator that can be expressed by a set of BSR formulas -- together with the usual objects of SMT solvers, notably integers, reals, uninterpreted symbols, enumerated types.
Type de document :
Communication dans un congrès
Bernhard Beckert. 4th International Verification Workshop - VERIFY'07, Jul 2007, Bremen, Germany. 259, pp.37-54, 2007, CEUR Workshop Proceedings
Liste complète des métadonnées

https://hal.inria.fr/inria-00186639
Contributeur : Pascal Fontaine <>
Soumis le : samedi 10 novembre 2007 - 14:57:57
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

  • HAL Id : inria-00186639, version 1

Collections

Citation

Pascal Fontaine. Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. Bernhard Beckert. 4th International Verification Workshop - VERIFY'07, Jul 2007, Bremen, Germany. 259, pp.37-54, 2007, CEUR Workshop Proceedings. 〈inria-00186639〉

Partager

Métriques

Consultations de la notice

175