Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Pascal Fontaine <>
Submitted on : Saturday, November 10, 2007 - 2:57:57 PM
Last modification on : Thursday, January 11, 2018 - 6:19:52 AM


  • HAL Id : inria-00186639, version 1



Pascal Fontaine. Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. 4th International Verification Workshop - VERIFY'07, Jul 2007, Bremen, Germany. pp.37-54. ⟨inria-00186639⟩



Record views