Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Being polite is not enough (and other limits of theory combination)

Guilherme V. Toledo, Benjamin Przybocki, Yoni Zohar

TL;DR

This paper demonstrates that politeness is not sufficient for theory combination by constructing decidable theories whose joint theory is undecidable, thereby clarifying limits of prominent combination methods such as Nelson–Oppen, gentle, polite, and shiny. It introduces finite-signature variants of key theories and provides finitized proofs, showing that the same limitation results hold under finite signatures. The authors also present two new combination theorems—one based on gentle with computable finite spectra and another on shininess without finite models—extending the toolkit for combining theories while preserving decidability. Collectively, the work sharpens our understanding of the necessary conditions for compositional decidability and offers practical avenues for enhancing SMT solvers with more flexible theory integration strategies. The results have significant implications for automated reasoning, formal verification, and the design of theory solvers in systems like $\textsf{cvc5}$ and related tools.

Abstract

In the Nelson-Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and the other has to satisfy a similar yet weaker property; in shiny combination, only one has to be shiny (smooth, with a computable minimal model function and the finite model property); and for polite combination, only one has to be strongly polite (smooth and strongly finitely witnessable). For each combination method, we prove that if any of its assumptions are removed, then there is no general method to combine an arbitrary pair of theories satisfying the remaining assumptions. We also prove new theory combination results that weaken the assumptions of gentle and shiny combination.

Being polite is not enough (and other limits of theory combination)

TL;DR

This paper demonstrates that politeness is not sufficient for theory combination by constructing decidable theories whose joint theory is undecidable, thereby clarifying limits of prominent combination methods such as Nelson–Oppen, gentle, polite, and shiny. It introduces finite-signature variants of key theories and provides finitized proofs, showing that the same limitation results hold under finite signatures. The authors also present two new combination theorems—one based on gentle with computable finite spectra and another on shininess without finite models—extending the toolkit for combining theories while preserving decidability. Collectively, the work sharpens our understanding of the necessary conditions for compositional decidability and offers practical avenues for enhancing SMT solvers with more flexible theory integration strategies. The results have significant implications for automated reasoning, formal verification, and the design of theory solvers in systems like and related tools.

Abstract

In the Nelson-Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and the other has to satisfy a similar yet weaker property; in shiny combination, only one has to be shiny (smooth, with a computable minimal model function and the finite model property); and for polite combination, only one has to be strongly polite (smooth and strongly finitely witnessable). For each combination method, we prove that if any of its assumptions are removed, then there is no general method to combine an arbitrary pair of theories satisfying the remaining assumptions. We also prove new theory combination results that weaken the assumptions of gentle and shiny combination.
Paper Structure (32 sections, 54 theorems, 19 equations, 4 figures, 5 tables)

This paper contains 32 sections, 54 theorems, 19 equations, 4 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. First-order logic
  4. Theory combination theorems
  5. Limitations of theory combination methods
  6. The theories that we use
  7. Nelson--Oppen and gentle combination
  8. Polite combination
  9. Shiny combination
  10. Finite signatures
  11. New theories over finite signatures
  12. Finitizing the proofs of \ref{['Nelson Oppen sharpness', 'theo:gentsharp', 'strong politeness sharpness SFW', 'ex:SHINYminusSM', 'strong politeness sharpness SM', 'shiny sharpness -CMMF', 'polite sharpness']}
  13. Finitizing the proof of \ref{['theo:SHINYminusSF']}
  14. New combination theorems
  15. Recovering gentle combination
  16. ...and 17 more sections

Key Result

theorem 1

$\mathcal{T}_{1}\oplus \mathcal{T}_{2}$ is decidable, if both $\mathcal{T}_1$ and $\mathcal{T}_2$ are stably infinite.

Figures (4)

  • Figure 1: An illustration of the contributions of RanRinZarJB10-LPARCADE and the current paper.
  • Figure 2: Cardinality formulas.
  • Figure 3: Formulas for the axiomatization of $\mathcal{T}_{f}$. $\overrightarrow{x}$ stands for $x_{1},\ldots,x_{n}$, and $p(x)$ for $s(x)=x$.
  • Figure 4: Formulas in $\Sigma_{t}^{a}$.

Theorems & Definitions (101)

  • theorem 1: NelsonOppen
  • theorem 2: JB10-LPAR
  • theorem 3: DBLP:journals/jar/TinelliZ05
  • theorem 4: gentle
  • theorem 5
  • proof : sketch
  • theorem 6
  • proof : sketch
  • theorem 7
  • proof : sketch
  • ...and 91 more