1
$\begingroup$

In the paper "Model-Based Theory Combination" (1) by De Moura and Bjorner they present an alternative to the Nelson-Oppen method for theory combination. They first describe the Nelson-Oppen combination method, which requires that the two theories being combined are 1) disjoint and 2) stably infinite. Then they describe model-based theory combination. Paraphrasing the intro of section 4:

Our approach minimizes the number of produced shared equalities. It is based on the fact that, in practice, the number of local inconsistencies is much bigger than the number of global (cross theory) inconsistencies. It works for convex and non-convex theories alike.

As stable infinity is not mentioned at all, I am inclined to believe that model-based theory combination can also combine non-stably infinite theories. Also the more detailed paragraphs after this do not mention stable infinity.

Empirically, this makes sense. Their SMT solver that implements this approach (Z3) supports bools as a value type. Booleans are effectively a bit vector of width one, and as the theory of bit vectors is the common example of a non-stably-infinite theory, supporting booleans means supporting & combining (at least one) non-stably infinite theory with other stably infinite theories.

If anyone can clarify, confirm, or falsify part of my explanation that'd be very appreciated! Because at the moment I'm stumped as to why stable infinity seems to be such an important requirement, while there is no source explaining how to deal with the finiteness of the boolean sort.

(I asked a relevant though different question here: 2. Since I cannot find a definition of stable infinity for many-sorted first order logic, I figured it's probably best to just ask about a clarification about an existing paper, than to further convolute my already existing question.)

$\endgroup$

1 Answer 1

1
$\begingroup$

A possible indirect answer can be found in slides (1) for a presentation for the 2008 Oregon Summer School on Logic and Theorem Proving by Leonardo de Moura, who worked on Z3 extensively:

Slide showing that non-stably infinite theories can be made stably-infinite by adding type information to all axioms

Essentially, I perceive the trick here to be that you add type information to all axioms. Then, it is safe to extend any interpretation found with infinite domains with elems that do not satisfy e.g. the is-bv predicate. I'm assuming Z3 uses this trick to support non-stably infinite theories; whether this implies that model-based theory combination does or does not rely on stable infinity, is not yet clear.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.