Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories

Abstract

In this survey, we report our recent work concerning combination results for interpolation and uniform interpolation in the context of quantifier-free fragments of first-order theories. We stress model-theoretic and algebraic aspects connecting this topic with amalgamation, strong amalgamation, and model-completeness. We give sufficient (and, in relevant situations, also necessary) conditions for the transfer of the quantifier-free interpolation property to combined first-order theories; we also investigate the non-disjoint signature case under the assumption that the shared theory is universal Horn. For convex, strong-amalgamating, stably infinite theories over disjoint signatures, we also provide a modular transfer result for the existence of uniform interpolants. Model completions play a key role in the whole paper: They enter into transfer results in the non-disjoint signature case and also represent a semantic counterpart of uniform interpolants.

1. Introduction

Craig’s interpolation theorem [1] is a classical well-known result in first-order logic; it says that whenever an implication

$$\varphi \to \psi$$

(1)

is valid, then there exists a formula $\theta$ such that the implications

$$\varphi \to \theta \mathrm{and}\theta \to \psi$$

(2)

are valid too, and the formula $\theta$ contains at most the symbols occurring both in $\varphi$ and in $\psi$. This theorem has been largely investigated both in propositional and predicate logics; a renewed interest in it has come from recent applications in verification [2,3,4]. The reason for why interpolation became important in verification is because it helps to discover, in a completely automatic way, new predicates that might contribute to the construction of invariants. In fact, many model-checking problems are of an infinite state, which means that the language needed in order to build, e.g., safety invariants, is quite rich and is far from requiring only finitely many formulae up to logical equivalence. Popular methods for synthesizing invariants analyze spurious error traces. Suppose that the system to be verified is specified via a triple $\langle \underline{x},\iota \left(\underline{x}\right),\tau (\underline{x},{\underline{x}}^{\prime })\rangle$ given by a tuple of variables $\underline{x}$, a formula $\iota \left(\underline{x}\right)$ describing initial states, and a formula $\tau (\underline{x},{\underline{x}}^{\prime })$ describing state evolutions; suppose also that we are given a further formula $\upsilon \left(\underline{x}\right)$ describing undesired ‘error’ states. Then, the system under examination cannot reach an error configuration in n steps iff the formula

$$\iota \left({\underline{x}}_0\right)\wedge \tau ({\underline{x}}_0,{\underline{x}}_1)\wedge \cdots \wedge \tau ({\underline{x}}_{n-1},{\underline{x}}_n)\wedge \upsilon \left({\underline{x}}_n\right)$$

is not satisfiable (in the models of a suitable theory T). From the unsatisfiability proof, taking an interpolant, say, at the i-th iteration, one can produce a formula $\theta \left(\underline{x}\right)$ such that, modulo T, we have that the implications

$$\iota \left({\underline{x}}_0\right)\wedge \underset{j=1}{\overset{i}{\bigwedge }}\tau ({\underline{x}}_{j-1},{\underline{x}}_j)\to \theta \left({\underline{x}}_i\right)\mathrm{and}\theta \left({\underline{x}}_i\right)\wedge \underset{j=i+1}{\overset{n}{\bigwedge }}\tau ({\underline{x}}_{j-1},{\underline{x}}_j)\wedge \upsilon \left({\underline{x}}_n\right)\to \perp$$

(3)

are both T-valid (i.e., true in all models of T). The formula $\theta$ (and the literals it contains) can contribute to the refinement of the current candidate safety invariant. This fact is exploited in different ways during invariant search; it can also be combined with orthogonal techniques in existing implementations, as witnessed by a rich literature; see, e.g., [4,5,6,7,8,9,10], among many other contributions.

One major problem encountered during the above applications concerns the shape of the interpolant. Usually, one considers implications such as (1), which are valid in all models of a given first-order theory T; but in general, there is no guarantee that if $\varphi ,\psi$ are both quantifier-free, then there is an interpolant $\theta$ such that the implications (2) are T-valid and such that $\theta$ is also quantifier-free. This is crucial because, very often, first-order theories commonly used in verification have a decidable quantifier-free fragment, but are undecidable outside that fragment (this is the case, for instance, of the McCarthy theory of arrays; see Section 3 below); even if general first-order satisfiability remains decidable, the computational cost of a satisfiability test may increase considerably when moving from the quantifier-free fragment to arbitrary first-order formulae (this is the case, for instance, of Presburger arithmetic). This is why some considerable effort has been put into designing theory-specific interpolation algorithms operating at a quantifier-free level [11,12,13,14,15,16,17] and in identifying suitable variants of theories axiomatizing common datatypes enjoying quantifier-free interpolation [18,19,20].

Still, knowing that an isolated theory by itself has quantifier-free interpolation might not be sufficient for applications; in common benchmarks, it happens that arrays, sets, lists, etc. are always arrays, sets, lists of something (booleans, integers, reals, etc.), so that one must be sure that quantifier-free interpolation transfers to combined theories. This will be the main subject of the first part of the present survey paper.

In the second part of the paper, we consider a strong form of Craig interpolation, namely, uniform interpolation. We recall here what uniform interpolants are in the context of the quantifier-free fragment of a first-order theory T. We use notations such as $\psi \left(\underline{x}\right)$ to say that at most the variables from the tuple $\underline{x}$ occur freely in $\psi$. Given a quantifier-free formula $\varphi (\underline{x},\underline{y})$, a uniform interpolant of $\varphi$ (w.r.t. $\underline{y}$) is a quantifier-free formula $\theta \left(\underline{x}\right)$ satisfying the following two properties:

• $\varphi (\underline{x},\underline{y})\to \theta \left(\underline{x}\right)$ is T-valid;
• For any further quantifier-free formula $\psi (\underline{x},\underline{z})$ such that $\varphi (\underline{x},\underline{y})\to \psi (\underline{x},\underline{z})$ is T-valid, we have that the implication $\theta \left(\underline{x}\right)\to \psi (\underline{x},\underline{z})$ is T-valid, too.

Whenever uniform interpolants exist, one can compute an interpolant for an entailment such as $\varphi (\underline{x},\underline{y})\to \psi (\underline{x},\underline{z})$ in a way that is independent of $\psi$. Uniform interpolants have been widely studied in the context of non-classical propositional logics (a non-exhaustive list includes [21,22,23,24,25,26,27,28]). In the last decade, the automated reasoning community has also developed an increasing interest in uniform interpolants, this time for quantifier-free fragments of first-order theories [29,30]; in this literature, uniform interpolants are often called ‘covers’, but the definitions of uniform interpolants and of covers are equivalent. In these contributions, examples of computations of uniform interpolants were supplied, and some algorithms were also sketched. The first formal proofs about the existence of uniform interpolants in $\mathcal{EUF}$ (the theory of pure equality in an arbitrary signature) were however published only in [31,32]. The usefulness of uniform interpolants in model checking was already stressed in [30] and further motivated by our recent line of research on the verification of data-aware processes [31,33,34,35]. In such applications, combination problems obviously arise, so in Section 5 below, we investigate transfer problems for uniform quantifier-free interpolation.

Structure of the Paper

Section 2 settles on notations and basic definitions. Section 3 investigates quantifier-free interpolation for combined theories in disjoint signatures and the semantic counterparts related to quantifier-free interpolation: amalgamation, strong amalgamation, and definability properties. Section 4 extends this analysis to the case of non-disjoint signature theories and shows interesting applications to modal logic. Section 5 introduces uniform interpolants, discusses their existence in $\mathcal{EUF}$ and shows how to transfer them to combined convex theories. Section 6 concludes.

The paper is conceived as a survey paper, principally addressed to a mathematical audience; however, it should be taken into account that many motivations and examples that suggested the results included in the paper come from the software verification area; hence, we give at least some sketches of algorithmic aspects. Proofs are omitted (sometimes in favor of intuitive justifications); however, they can all be found in the original papers. More precisely, proofs of the results from Section 3 are in [36], proofs of the results from Section 4 are in [37], and proofs of the results from Section 5 are in [31,32,38,39,40].

2. Preliminaries

We assume that the reader is familiar with the basic notions concerning first-order logic; this includes syntactic notions such as signature, variable, term, atom, literal, formula, and sentence and semantic notions such as structure, substructure, truth, satisfiability, and validity. The equality symbol “=” is considered a logical symbol and, hence, is included in all signatures considered below; to exclude limit cases, we always assume that our signatures always contain at least one individual constant symbol. When we use notations such as $E\left(\underline{x}\right)$, we mean that the expression (term, literal, formula, etc.) E contains free variables only from the tuple $\underline{x}$. Concerning ‘tuples’, we make an important convention: When we speak of a ‘tuple of variables’, the tuple is meant to represent an arity; hence, it is assumed not to contain repetitions. The same convention does not apply when we speak of a ‘tuple of terms’, which might consequently contain repetitions. These conventions are useful for substitutions; we use them when denoting with $\varphi (\underline{t}/\underline{x})$ the formula obtained from $\varphi \left(\underline{x}\right)$ by the simultaneous replacement of the ‘tuple of variables’ $\underline{x}$ with the ‘tuple of terms’ $\underline{t}$. For similar reasons, whenever we use a notation such as $E(\underline{x},\underline{y})$, we assume not only that the tuples $\underline{x}$ and $\underline{y}$ are made of pairwise distinct elements, but also that $\underline{x}$ and $\underline{y}$ are disjoint as sets. A formula is universal (existential) iff it is obtained from a quantifier-free formula by prefixing it with a string of universal (or existential) quantifiers. A formula is ground iff it does not contain occurrences of variables (neither free nor bound).

From the semantic side, we refer to standard model-theoretic terminology [41] for basic notions such as structures, embeddings, diagrams, etc. $\mathsf{\Sigma }$-structures are indicated with calligraphic letters $\mathcal{A},\mathcal{B},\cdots ,\mathcal{M},\mathcal{N},\cdots$; the support of a $\mathsf{\Sigma }$-structure $\mathcal{A}$ is indicated with $\left|\mathcal{A}\right|$. A theory T in a signature $\mathsf{\Sigma }$ is a set of $\mathsf{\Sigma }$-sentences; the models of T are those $\mathsf{\Sigma }$-structures in which all the sentences in T are true. A $\mathsf{\Sigma }$-formula $\varphi$ is T-satisfiable (or T-consistent) if there exists a model $\mathcal{M}$ of T such that $\varphi$ is true in $\mathcal{M}$ under a suitable assignment $\mathtt{a}$ to the free variables of $\varphi$ (in symbols, $(\mathcal{M},\mathtt{a})\vDash \varphi$); it is T-valid (in symbols, $T⊢\phi$) if its negation is not T-satisfiable. A theory T is universal iff all sentences in T are universal. A theory T admits quantifier-elimination iff, for every formula $\varphi \left(\underline{x}\right)$, there is a quantifier-free formula ${\varphi }^{\prime }\left(\underline{x}\right)$ such that $T⊢\varphi \leftrightarrow {\varphi }^{\prime }$ (since we work in a computational logic context, we consider part of the definition of a theory enjoying quantifier elimination the fact that such ${\varphi }^{\prime }$ is effectively computable from $\varphi$). A formula ${\phi }_1$T-entails a formula ${\phi }_2$ if the implication ${\phi }_1\to {\phi }_2$ is T-valid (in symbols, ${\phi }_1{⊢}_T{\phi }_2$, or simply ${\phi }_1⊢{\phi }_2$ when T is clear from the context). If $\Gamma$ is a set of formulæ and $\varphi$ is a formula, the notation $\Gamma {⊢}_T\varphi$ means that there are ${\gamma }_1,\cdots ,{\gamma }_n\in \Gamma$ such that ${\gamma }_1\wedge \cdots \wedge {\gamma }_n{⊢}_T\varphi$. The satisfiability modulo the theory T (SMT$\left(T\right)$) problem amounts to establishing the T-satisfiability of quantifier-free $\mathsf{\Sigma }$-formulæ. Some theories have special standard names in the SMT-literature (some of these names will be recalled during the paper). For pure equality theory, our conventions are as follows. We shall call $\mathcal{EUF}\left(\mathsf{\Sigma }\right)$ the pure equality theory in the signature $\mathsf{\Sigma }$; we may also use just $\mathcal{EUF}$ instead of $\mathcal{EUF}\left(\mathsf{\Sigma }\right)$ in case there is no need to specify the signature $\mathsf{\Sigma }$; however, in that case, $\mathsf{\Sigma }$ is assumed to be proper, i.e., it must contain (besides free constants) at least a predicate or a function symbol different from equality.

2.1. Combinations of Theories

Stable infiniteness is a semantic ingredient often occurring in combination results; the requirement is rather mild, and most theories used in verification, such as theories axiomatizing fragments of arithmetics as well as common datatypes, satisfy it (but there are also notable exceptions, such as bitvector theories). The formal definition is as follows. A theory T is stably infinite iff every T-satisfiable quantifier-free formula (from the signature of T) is satisfiable in an infinite model of T. By compactness, it is immediate to show that T is stably infinite iff every model of T embeds into an infinite one.

Let $T_i$ be a stably infinite theory over the signature ${\mathsf{\Sigma }}_i$ such that the $SMT\left(T_i\right)$ problem is decidable for $i=1,2$ and ${\mathsf{\Sigma }}_1$ and ${\mathsf{\Sigma }}_2$ are disjoint (i.e., the only shared symbol is equality). Under these assumptions, the Nelson–Oppen combination method [42,43] tells us that the SMT problem for the combination $T_1\cup T_2$ of the theories $T_1$ and $T_2$ (i.e., the union of their axioms) is decidable. In general, however, the combined SMT problem $T_1\cup T_2$ may become undecidable, even when the $SMT\left(T_1\right),SMT\left(T_2\right)$ problems are decidable and the signatures are disjoint [44]; on the other hand, stable infiniteness is a sufficient but not necessary condition for the decidability transfer of $SMT$ problems to a disjoint combination (for a survey on different sufficient criteria, see [45], and for recent developments, also see [46]).

2.2. Interpolation Properties

In this paper, we are interested in specializing the Craig interpolation property to quantifier-free fragments of first-order theories. We give two definitions: The first one is more restricted, and the second one is more liberal.

Definition 1.

[Plain quantifier-free interpolation] A theory T admits (plain) quantifier-free interpolation (or, equivalently, has quantifier-free interpolants) iff, for every pair of quantifier-free formulae $\varphi (\underline{x},\underline{y}),\psi (\underline{y},\underline{z})$ such that $\psi {⊢}_T\varphi$, there exists a quantifier-free formula $\theta \left(\underline{y}\right)$, called an interpolant, such that: (i) $\psi {⊢}_T\theta$, (ii) $\theta {⊢}_T\varphi$. (Notice that only the variables $\underline{y}$ occurring in both ψ and ϕ can occur in θ.)

The following extension of the above definition is considered more natural (and also more useful in verification applications):

Definition 2.

[General quantifier-free interpolation] Let T be a theory in a signature Σ; we say that T has the general quantifier-free interpolation property iff, for every signature ${\mathsf{\Sigma }}^{\prime }$ (disjoint from Σ) and for every pair of ground $\mathsf{\Sigma }\cup {\mathsf{\Sigma }}^{\prime }$-formulæ $\varphi ,\psi$ such that $\psi {⊢}_T\varphi$, there exists a ground formula θ, such that: (i) $\psi {⊢}_T\theta$, (ii) $\theta {⊢}_T\varphi$, and (iii) all predicates, constants, and function symbols from ${\mathsf{\Sigma }}^{\prime }$ occurring in θ also occur both in ϕ and ψ.

Since free variables can be replaced by free constants without affecting entailment relations, it should be clear that the general quantifier-free interpolation property (Definition 2) implies the plain quantifier-free interpolation property (Definition 1).

2.3. Amalgamation Properties

When stating amalgamability and strong amalgamability properties (see [47] for a survey), people usually limit themselves to universal theories; actually, most theories we have in mind for several applications are universal; however, to some extent, we also want to handle general first-order theories in the paper. In order to do that, it is important to observe that a substructure of a model of a non-universal theory need not be a model of the theory. Thus, in our definitions, we must take into account substructures that are not necessarily submodels. This leads to the notions below, which we call ‘sub-amalgamability’ and ‘strong sub-amalgamability’:

Definition 3.

Let T be a theory; we call a T-fork a triple $({\mathcal{M}}_1,{\mathcal{M}}_2,\mathcal{A})$, where ${\mathcal{M}}_1,{\mathcal{M}}_2$ are models of T and $\mathcal{A}$ is their shared substructure. (By this, we mean that $\mathcal{A}$ is a substructure of both ${\mathcal{M}}_{1}and{\mathcal{M}}_2$ and that $\left|\mathcal{A}\right|=|{\mathcal{M}}_1|\cap |{\mathcal{M}}_2|$.) AT-amalgam of such a fork is a triple $(\mathcal{M},{\mu }_1,{\mu }_2)$, where $\mathcal{M}$ is a T-model and ${\mu }_1:{\mathcal{M}}_1⟶\mathcal{M}$, ${\mu }_2:{\mathcal{M}}_2⟶\mathcal{M}$ are embeddings whose restrictions to the support of $\mathcal{A}$ coincide. A theory T has the sub-amalgamation property iff every T-fork has a T-amalgam.

A theory T has the strong sub-amalgamation property iff every T-fork $({\mathcal{M}}_1,{\mathcal{M}}_2,\mathcal{A})$ has a T-amalgam $(\mathcal{M},{\mu }_1,{\mu }_2)$ satisfying the following additional condition: If for some $m_1\in |{\mathcal{M}}_1|,m_2\in \left|{\mathcal{M}}_2\right|$, we have ${\mu }_1\left(m_1\right)={\mu }_2\left(m_2\right)$, then there exists an element a in $\left|\mathcal{A}\right|$ such that $m_1=a=m_2$.

When the theory T is universal, we may speak of ‘amalgamation’ and ‘strong amalgamantion’ properties instead of ‘sub-amalgamation’ and ‘strong sub-amalgamation’ properties, respectively.

3. Strong Amalgamation and Combined Interpolation

The results presented in this section concern the relationships between syntactical notions, such as forms of interpolation, and their corresponding semantic counterparts, such as variants of amalgamation, and they are based on [36]. An old result due to Bacsich [48] connects quantifier-free interpolation and amalgamation for the case of universal theories; the result can be easily extended to arbitrary first-order theories replacing amalgamation with sub-amalgamation [36].

Theorem 1

[36,48]. A theory T has the sub-amalgamation property iff it admits quantifier-free interpolants.

The above theorem can be used to find examples and counterexamples. For instance, it is easily seen that $\mathcal{EUF}$ (which is trivially universal) has amalgamation, and hence, it has quantifier-free interpolants; in fact, $\mathcal{EUF}$ also has the strong amalgamation property mentioned above. A simple example of a universal theory that does not enjoy amalgamation is the theory of a binary relation that is a partial function.

Less trivial examples and counterexamples are given by the variants of McCarthy’s theory of arrays [49]. We consider three variants of this theory. The first variant is ${\mathcal{AR}}_{\mathrm{ext}}$, which is the theory of arrays with extensionality. The signature of ${\mathcal{AR}}_{\mathrm{ext}}$ contains the sort symbols $\mathtt{ARRAY},\mathtt{ELEM}$, and $\mathtt{INDEX}$ and the function symbols $rd:\mathtt{ARRAY}\times \mathtt{INDEX}⟶\mathtt{ELEM}$ and $wr:\mathtt{ARRAY}\times \mathtt{INDEX}\times \mathtt{ELEM}⟶\mathtt{ARRAY}$. (notice that Theorem 1, and in general all results in this paper, extends to many-sorted signatures). The set of axioms of ${\mathcal{AR}}_{\mathrm{ext}}$ consists of the following three sentences:

$$\begin{array}{cc}\hfill & \forall y,i,j,e.i\ne j\to rd\left(wr\right(y,i,e),j)=rd(y,j),\end{array}$$

(4)

$$\begin{array}{cc}\hfill & \forall y,i,e.rd\left(wr\right(y,i,e),i)=e,\end{array}$$

(5)

$$\begin{array}{cc}\hfill & \forall x,y.x\ne y\to (\exists i.rd(x,i)\ne rd(y,i\left)\right)\end{array}$$

(6)

Now, ${\mathcal{AR}}_{\mathrm{ext}}$ enjoys the amalgamation property in the sense that, given two models ${\mathcal{M}}_1$ and ${\mathcal{M}}_2$ of ${\mathcal{AR}}_{\mathrm{ext}}$ sharing a substructure ${\mathcal{M}}_0$that is also a model of${\mathcal{AR}}_{\mathrm{ext}}$, there is a model $\mathcal{M}$ of ${\mathcal{AR}}_{\mathrm{ext}}$ endowed with embeddings from ${\mathcal{M}}_1,{\mathcal{M}}_2$ agreeing on the support of ${\mathcal{M}}_0$. However, ${\mathcal{AR}}_{\mathrm{ext}}$ is not universal, so this is not sufficient to guarantee quantifier-free interpolation. In fact, ${\mathcal{AR}}_{\mathrm{ext}}$ is not sub-amalgamable, and quantifier-free interpolation fails for it, as shown by the following valid implication whose interpolants require a quantifier (the counterexample is due to R. Jhala and is reported in [50]):

$$a=wr(b,i,e)\to \neg (j_1\ne j_2\wedge rd(a,j_1)\ne rd(b,j_1)\wedge rd(a,j_2)\ne rd(b,j_2)).$$

(7)

The theory ${\mathcal{AX}}_{\mathtt{diff}}$ is obtained from ${\mathcal{AR}}_{\mathrm{ext}}$ by skolemizing the extensionality axiom (6); hence, its language has an extra binary function $\mathtt{diff}:\mathtt{ARRAY}\times \mathtt{ARRAY}⟶\mathtt{INDEX}$ and the following additional axiom:

$$\begin{array}{ccc}\hfill \forall x,y.& & x\ne y\to rd(x,\mathtt{diff}(x,y\left)\right)\ne rd(y,\mathtt{diff}(x,y\left)\right).\hfill \end{array}$$

(8)

which replaces (6). This theory is universal and (strongly) amalgamable [18,19]. This means that quantifier-free interpolants exist; for example, an interpolant of the two formulæ (8) can be written without quantifiers in this theory as

$$a=wr(b,\mathtt{diff}(a,b),rd(b,\mathtt{diff}(a,b)\left)\right).$$

The third variant of the array theory we want to mention is the theory ${\mathcal{AX}}_{maxdiff}$, where the axiom (8) is strengthened so that $\mathtt{diff}(a,b)$ returns the biggest index where $a,b$ differ. This requires adding at least a symbol for a total ordering relation on the sort $\mathtt{INDEX}$ (we leave the reader to consult [20] for details). Under suitable mild hypotheses, it is possible to prove that the universal theory ${\mathcal{AX}}_{maxdiff}$ also has amalgamation and, hence, quantifier-free interpolation (but the proof is surprisingly much more delicate [20]).

Amalgamation and sub-amalgamation are not modular properties in the sense that they can get lost when taking union of theories, even under disjoint signatures. However, strong amalgamation, under stable infiniteness, is modular [36].

Theorem 2

[36]. Let $T_1$ and $T_2$ be two stably infinite theories over disjoint signatures ${\mathsf{\Sigma }}_1$ and ${\mathsf{\Sigma }}_2$. If both $T_1$ and $T_2$ have the strong sub-amalgamation property, then so does $T_1\cup T_2$. Thus, in view of Theorem 1, $T_1\cup T_2$ has quantifier-free interpolants.

Actually, strong sub-amalgamation is a necessary condition for the transfer of the quantifier-free interpolation property in the sense that is precisely stated in the following result.

Theorem 3

[36]. Let T be a theory admitting quantifier-free interpolation and let Σ be a proper signature disjoint from the signature of T. Then, $T\cup \mathcal{EUF}\left(\mathsf{\Sigma }\right)$ has quantifier-free interpolation iff T has the strong sub-amalgamation property.

The intuitive reason for why the above theorem holds is the following. Recall that since $\mathsf{\Sigma }$ is proper, it must contain at least a function or a predicate symbol different from equality. Suppose, e.g., it contains a unary predicate P; take models ${\mathcal{M}}_1,{\mathcal{M}}_2$ of T that cannot be strongly amalgamated over their common substructure. Then, expand them to $\mathsf{\Sigma }$-structures in such a way that P holds precisely for the elements of the support of ${\mathcal{M}}_1$ that are not from the support of ${\mathcal{M}}_2$; clearly, sub-amalgamation fails for these expanded models; hence, $T\cup \mathcal{EUF}\left(\mathsf{\Sigma }\right)$ lacks quantifier-free interpolation.

Strong amalgamation also characterizes the general quantifier-free interpolation property.

Theorem 4

[36]. A theory T has the general quantifier-free interpolation property iff T has the strong sub-amalgamation property.

3.1. Strong Amalgamation: A Syntactic Characterization

Strong amalgamation needs an ‘operational’ characterization to be useful when designing concrete combined interpolation algorithms. We reformulate strong amalgamation via a syntactic property (to be called the equality-interpolating property); this syntactic property, roughly speaking, says that disjunctions of variables’ equalities can be entailed, modulo T, by quantifier-free formulae only in the case that such equalities are mediated by explicitly defining terms.

Given two finite tuples $\underline{t}\equiv t_1,\cdots ,t_n$ and $\underline{v}\equiv v_1,\cdots ,v_m$ of terms,

$$\begin{array}{c}\hfill \mathrm{the}\mathrm{notation}\underline{t}\cap \underline{v}\ne \varnothing \mathrm{stands}\mathrm{for}\mathrm{the}\mathrm{formula}\underset{i=1}{\overset{n}{\bigvee }}\underset{j=1}{\overset{m}{\bigvee }}(t_i=v_j).\end{array}$$

We use ${\underline{t}}_1{\underline{t}}_2$ to denote the juxtaposition of the two tuples ${\underline{t}}_1$ and ${\underline{t}}_2$ of terms. So, for example, ${\underline{t}}_1{\underline{t}}_2\cap \underline{v}\ne \varnothing$ is equivalent to $({\underline{t}}_1\cap \underline{v}\ne \varnothing )\vee ({\underline{t}}_2\cap \underline{v}\ne \varnothing )$. Next Definition is taken from [36] [Definition 4.1 and Theorem 4.2(iii)]:

Definition 4.

A theory T is equality interpolating iff it has the quantifier-free interpolation property and satisfies the following condition:

•

for every triple $\underline{x},{\underline{y}}_1,{\underline{y}}_2$ of tuples of variables and for every pair of quantifier-free formulae ${\delta }_1(\underline{x},{\underline{y}}_1),{\delta }_2(\underline{x},{\underline{y}}_2)$ such that

$${\delta }_1(\underline{x},{\underline{y}}_1)\wedge {\delta }_2(\underline{x},{\underline{y}}_2){⊢}_T{\underline{y}}_1\cap {\underline{y}}_2\ne \varnothing$$

(9)

there exists a tuple $\underline{v}\left(\underline{x}\right)$ of terms such that

$${\delta }_1(\underline{x},{\underline{y}}_1)\wedge {\delta }_2(\underline{x},{\underline{y}}_2){⊢}_T{\underline{y}}_1{\underline{y}}_2\cap \underline{v}\ne \varnothing .$$

(10)

The following theorem states the syntactic counterpart of the strong amalgamation property.

Theorem 5

[36]. Given a theory T with quantifier-free interpolation, the following conditions are equivalent:

(i)

T is strongly sub-amalgamable;

(ii)

T is equality interpolating.

If a theory T has quantifier elimination, then it obviously also has quantifier-free interpolants, and hence, it is sub-amalgamable. However, quantifier elimination is not sufficient to get strong sub-amalgamation (see below for counterexamples). Nevertheless, if the theory is also universal, then quantifier elimination is sufficient.

Theorem 6

[36]. A universal theory admitting quantifier elimination is equality interpolating.

Proof. 

(Sketch) In order to prove this theorem, one needs to preliminarily show a testing-point quantifier elimination lemma; such a lemma says that if T is universal and has quantifier elimination, then for every quantifier-free formula $\varphi (\underline{x},\underline{y})$, there exists a tuple ${\underline{t}}_1\left(\underline{x}\right),\cdots ,{\underline{t}}_n\left(\underline{x}\right)$ of tuples of terms such that

$$T⊢\exists \underline{y}\varphi (\underline{x},\underline{y})\leftrightarrow \underset{i=1}{\overset{n}{\bigvee }}\varphi (\underline{x},{\underline{t}}_i\left(\underline{x}\right)).$$

(11)

Taking this preliminary result for granted, we formally prove that a universal and quantifier eliminable theory T satisfies the implication (9)$\Rightarrow$(10). Suppose that (9) holds; by the testing-point quantifier elimination lemma, there exist tuples of terms ${\underline{t}}_1\left(\underline{x}\right),\cdots ,{\underline{t}}_k\left(\underline{x}\right)$ such that

$$\exists {\underline{y}}_2{\delta }_2(\underline{x},{\underline{y}}_2)\leftrightarrow \underset{j=1}{\overset{k}{\bigvee }}{\delta }_2(\underline{x},{\underline{t}}_j\left(\underline{x}\right))$$

(12)

is T-valid. For every $j=1,\cdots ,k$, if we replace ${\underline{y}}_2$ with ${\underline{t}}_j$ in (9), we get

$${\delta }_1(\underline{x},{\underline{y}}_1)\wedge {\delta }_2(\underline{x},{\underline{t}}_j){⊢}_T{\underline{y}}_1\cap {\underline{t}}_j\ne \varnothing$$

and, hence,

$${\delta }_1(\underline{x},{\underline{y}}_1)\wedge \underset{j=1}{\overset{k}{\bigvee }}{\delta }_2(\underline{x},{\underline{t}}_j){⊢}_T\underset{j=1}{\overset{k}{\bigvee }}({\underline{y}}_1\cap {\underline{t}}_j\ne \varnothing ).$$

Taking into account (12) and letting $\underline{v}$ be the tuple ${\underline{t}}_1\cdots {\underline{t}}_k$ obtained by juxtaposition, we get

$${\delta }_1(\underline{x},{\underline{y}}_1)\wedge \exists {\underline{y}}_2{\delta }_2(\underline{x},{\underline{y}}_2){⊢}_T{\underline{y}}_1\cap \underline{v}\ne \varnothing .$$

Removing the existential quantifier in the antecedent of the implication, we obtain

$${\delta }_1(\underline{x},{\underline{y}}_1)\wedge {\delta }_2(\underline{x},{\underline{y}}_2){⊢}_T{\underline{y}}_1\cap \underline{v}\ne \varnothing$$

and, a fortiori, $\left(10\right)$, as desired. □

Theorem 6 immediately yields a bunch of strongly amalgamating theories.

Example 1.

The theory $\mathcal{RDS}$ of recursive data structures [51] requires a signature comprising two unary function symbols ‘$car$’ and ‘$cdr$’ and a binary function symbol ‘$cons$’; the axioms of $\mathcal{RDS}$ are the following:

$$\begin{array}{c}\hfill \forall x,y.car\left(cons\right(x,y\left)\right)=x,\end{array}$$

(13)

$$\begin{array}{c}\hfill \forall x,y.cdr\left(cons\right(x,y\left)\right)=y,\end{array}$$

(14)

$$\begin{array}{c}\hfill \forall x,y.cons\left(car\right(x),cdr(x\left)\right)=x,\end{array}$$

(15)

$$\begin{array}{c}\hfill \forall x.x\ne t\left(x\right),\end{array}$$

(16)

where t is a term obtained by finitely many applications of $car$ and $cdr$ to the variable x (e.g., axioms (16) include $\forall x.car\left(x\right)\ne x$, $\forall x.cdr\left(cdr\right(x\left)\right)\ne x$, $\forall x.cdr\left(car\right(x\left)\right)\ne x$, and so on). Clearly, $\mathcal{RDS}$ is universal; the fact that it admits elimination of quantifiers has been known since an old work by Mal’cev [52].

Example 2.

The theory $\mathcal{IDL}$ of integer difference logic requires a signature comprising the constant symbol ‘0’, the unary function symbols ‘$succ$’ and ‘$pred$’, and the binary predicate symbol ‘<’; it is axiomatized by adding to the irreflexivity, transitivity, and linearity axioms for < the following set of sentences:

$$\begin{array}{c}\hfill \begin{array}{cc}\forall x.succ\left(pred\right(x\left)\right)=x,\hfill & \forall x.pred\left(succ\right(x\left)\right)=x,\hfill \\ \forall x,y.x<succ\left(y\right)\leftrightarrow (x<y\vee x=y),\hfill & \forall x,y.pred\left(x\right)<y\leftrightarrow (x<y\vee x=y).\hfill \end{array}\end{array}$$

$\mathcal{IDL}$ is universal, and the fact that admits elimination of quantifiers can be shown by slightly modifying the procedure for the similar theory of natural numbers with successor and ordering in [53]. Notice that the atoms of $\mathcal{IDL}$ are equivalent to formulae of the form $i\bowtie f^n\left(j\right)$, where

(a)

$n\in \mathbb{Z}$ and $\bowtie \in \{=,<\}$;

(b)

$i,j$ are variables or the constant 0;

(c)

$f^0\left(j\right)$ is j, $f^k\left(j\right)$ abbreviates $succ\left(suc{c}^{k-1}\left(j\right)\right)$ when $k>0$ or $pred\left(pre{d}^{k-1}\left(j\right)\right)$ when $k<0$.

Usually, $i\bowtie f^n\left(j\right)$ is written as $i-j\bowtie n$ or as $i\bowtie j+n$; hence, the name of “integer difference logic.”

Example 3.

The theory $\mathcal{UTVPI}$ is a fragment of linear arithmetic over the integers that is slightly more expressive than $\mathcal{IDL}$. It can be defined as the theory whose axioms are the sentences that are true in $\mathbb{Z}$ in the signature comprising the constant 0, the unary function symbols $pred$, $succ$, and −, and the binary predicate symbol <. It can be shown that $\mathcal{UTVPI}$ has a set of quantifier-eliminating universal axioms [36]; thus, $\mathcal{UTVPI}$ is equality interpolating.

Example 4.

Linear Arithmetic over the Reals can be axiomatized as the theory of totally ordered divisible abelian groups [41]. It has quantifier elimination (e.g., via the Fourier–Motzkin procedure), but it is easily seen that it is not strongly sub-amalgamable (just consider two copies of the reals sharing the integers as a common substructure). However, if one includes multiplication by rational coefficients in the signature of the theory, one gets a universal set of axioms enjoying quantifier elimination, thus gaining strong amalgamation and the equality-interpolating property.

Example 5.

The situation is somewhat similar for integer linear arithmetics. The theory of the integers under addition, 0, successor, and ordering does not have quantifier elimination; if we add infinitely many unary predicates for equivalence modulo n, we get Presburger arithmetics that enjoy quantifier elimination. However, this is not yet sufficient for the equality-interpolating property; for that, we must add infinitely many unary function symbols for integer division by n, varying n (see [36] or [54] for details).

3.2. The Case of Convex Theories

A first-order theory T is said to be convex iff, for every conjunction of literals $\delta$ if

$$\delta {⊢}_T\underset{i=1}{\overset{n}{\bigvee }}{x}_i=y_i,$$

then there is $i=1,\cdots ,n$ such that

$$\delta {⊢}_T{x}_i=y_i.$$

Among convex theories, we have universal Horn theories (see Section 4 below); another remarkable example of a convex theory is linear real arithmetic (here is where the name ‘convex’ comes from: It comes from the fact that the convexity of linear real arithmetic follows from the geometrical fact that if a convex set is contained in a union of hyperplanes, then it is contained in one of them). On the other hand, integer linear arithmetic (Example 5) and integer difference logic (Example 2) are non-convex theories.

In convex theories, one can formulate the equality-interpolating condition in some interesting simpler ways. A formula is said to be primitive iff it is obtained by prefixing some existential quantifiers to a conjunction of literals.

Proposition 1

[36]. The following conditions are equivalent for a convex theory T with quantifier-free interpolation:

(i)

T is equality interpolating;

(ii)

For every pair $y_1,y_2$ of variables and for every pair of conjunctions of literals ${\delta }_1(\underline{x},{\underline{z}}_1,y_1)$, ${\delta }_2(\underline{x},{\underline{z}}_2,y_2)$ such that

$${\delta }_1(\underline{x},{\underline{z}}_1,y_1)\wedge {\delta }_2(\underline{x},{\underline{z}}_2,y_2){⊢}_T{y}_1=y_2$$

(17)

there exists a term $v\left(\underline{x}\right)$ such that

$${\delta }_1(\underline{x},{\underline{z}}_1,y_1)\wedge {\delta }_2(\underline{x},{\underline{z}}_2,y_2){⊢}_T{y}_1=v\left(\underline{x}\right)\wedge y_2=v\left(\underline{x}\right).$$

(18)

(iii)

For every tuple of variables $\underline{x}$, for every further variable y, and for every primitive formula $\delta (\underline{x},y)$ such that

$$\delta (\underline{x},y^{\prime })\wedge \delta (\underline{x},y^{″}){⊢}_T{y}^{\prime }=y^{″}$$

there is a term $v\left(\underline{x}\right)$ such that

$$\delta (\underline{x},y){⊢}_{T}y=v\left(\underline{x}\right).$$

Condition (ii) is due to Yorsh and Musuvathi; in fact, in [55], they proved the combination Theorem 2 for the restricted case of convex theories using precisely condition (ii) instead of the semantic notion of strong sub-amalgamation. Condition (iii) is the Beth definability property formulated for the primitive fragment of the language—we shall call it the primitive Beth definability property (modulo T). We shall make use of this property in Section 5.2 when we discuss an algorithm for computing combined uniform interpolants in the convex case.

3.3. Sketch of the Combined Interpolation Algorithm

Theorem 2 shows that the union of two stably infinite signature-disjoint strongly amalgamable theories has the quantifier-free interpolation property. However, it does not show how to compute quantifier-free interpolants given analogous input algorithms for the component theories. Such an algorithm is described in detail in [36]; we give some indications here of how it works.

Below, we consider two theories $T_1,T_2$ in their respective signatures ${\mathsf{\Sigma }}_1,{\mathsf{\Sigma }}_2$; the two theories are both stably infinite and equality interpolating; moreover, the $SMT\left(T_1\right),SMT\left(T_2\right)$ problems are decidable and the signatures ${\mathsf{\Sigma }}_1,{\mathsf{\Sigma }}_2$ are disjoint. We also assume the availability of algorithms for $T_1$ and $T_2$ that are able not only to compute quantifier-free interpolants, but also the tuples $\underline{v}$ of terms in Definition 4 for the equality-interpolating property. Since the $SMT\left(T_i\right)$ problem is decidable for $i=1,2$, it is always possible to build an equality-interpolating algorithm by enumeration; in practice, better algorithms can be designed (see [55] for some examples concerning convex theories, see above for non-convex examples regarding some quantifier-eliminating arithmetic theories).

We can restate our problem as follows: We are given a finite set $A_0$ and a finite set $B_0$ of ${\mathsf{\Sigma }}_1\cup {\mathsf{\Sigma }}_2$-ground formulae possibly containing additional free constants. We assume that $A_0\wedge B_0$ is $T_1\cup T_2$-unsatisfiable (here, by abuse of notation, we confuse a finite set of formulae with its conjunction). We must find a finite set of ground formulae C (containing at most the free constants occurring both in $A_0$ and in $B_0$) such that $A_0{⊢}_{T_1\cup T_2}C$ and $C\wedge B_0{⊢}_{T_1\cup T_2}\perp$. Applying standard purification procedures, we can assume that all literals in $A_0,B_0$ are pure, meaning that they cannot contain both an A-strict free constant and a B-strict free constant. Here, we call A-strict (or B-strict) a free constant occurring only in $A_0$ (or only in $B_0$); we call it ‘shared’ if it occurs in both $A_0$ and $B_0$. Finally, we call it A-local (or B-local) iff it is either shared or A-strict (or B-strict). A similar terminology is applied to terms, literals, and quantifier-free formulæ; they are said to be A-local, B-local or shared iff they contain only constants that are A-local, B-local or shared, respectively.

The algorithm uses the metarules framework introduced in [18]. This framework collects some manipulations that can be freely operated in pairs $(A,B)$ without losing the possibility of computing an interpolant. For instance, if $A⊢{\bigvee }_{k=1}^n{\psi }_k$, where the ${\psi }_k$ are A-local, then it is possible to non-deterministically replace A with $A\cup \left\{{\psi }_k\right\}$, compute all interpolants of $(A\cup \left\{{\psi }_k\right\},B)$, and then recombine them into an interpolant of $(A,B)$. A long list of metarules is supplied in [18,36]; they are rather simple transformations. Strictly speaking, metarules are not part of an interpolation algorithm; however, if every single transformation of a concrete interpolation algorithm can be reformulated as a combination of metarules, then the algorithm itself is automatically partially correct (that is, it gives a correct answer when it terminates), and only termination requires a proof in order to achieve its total correctness.

The combined interpolation algorithm we are introducing follows this schema. It manipulates $A_0,B_0$ by applying transformation rules (justified by metarules) that generate a tree labeled by pairs $(A,B)$. In the end, it will be possible to compute, via the input interpolation algorithms, an interpolant out of every leaf; such interpolants will then be re-combined to form an interpolant for the original unsatisfiable pair $A_0,B_0$. While applying the transformation rules, it might happen that some A-strict free constant a ‘becomes shared’ because an equation $a=t$ explicitly defining it via a shared term is entailed by the current A; the same might happen for a B-strict constant. This ‘term-sharing’ technique is easily justified by a combination of metarules.

Now, one of the transformation rules simply guesses a Boolean assignment satisfying the current formula A (or B) and adds the corresponding set of literals to A (or B). A Boolean assignment can also guess equalities or disequalities among A-strict (or B-strict) constants, between an A-strict (or B-strict) constant and a shared constant, or between two shared constants. What the assignment cannot do is guess an equality/disequality between an A-strict and a B-strict constant because no impure literal is tolerated in the interpolant to be built. So, it is assumed by default that A-strict and B-strict constants cannot be equal to each other. When this leads to an inconsistency, this is just because a relation such as

$$\begin{array}{c}\hfill A_i\cup B_i{⊢}_{T_i}\underline{a}\cap \underline{b}\ne \varnothing \end{array}$$

holds for $i=1$ or $i=2$ (here, $\underline{a}=a_1,\cdots ,a_n$ are the A-strict constants, $\underline{b}=b_1,\cdots ,b_m$ are the B-strict constants, and $A_i$, $B_i$ are those among the currently assigned literals that are ${\mathsf{\Sigma }}_i$-literals). If this happens, by the equality-interpolating property, there are shared terms $\underline{v}=v_1,\cdots ,v_p$ such that

$$\begin{array}{c}\hfill A_i\cup B_i{⊢}_{T_i}(\underline{a}\cap \underline{v}\ne \varnothing )\vee (\underline{b}\cap \underline{v}\ne \varnothing ).\end{array}$$

Invoking the available interpolation algorithm for $T_i$, we can compute a ground shared ${\mathsf{\Sigma }}_i$-formula $\theta$ such that $A{⊢}_{T_i}\theta \vee \underline{a}\cap \underline{v}\ne \varnothing$ and $\theta \wedge B{⊢}_{T_i}\underline{b}\cap \underline{v}\ne \varnothing$. We choose among $n\ast p+m\ast p$ alternatives in order to non-deterministically update $A,B$ in the successor nodes. For the first $n\ast p$ alternatives, we add some $a_i=v_j$ (for $1\le i\le n$, $1\le j\le p$) to A. For the last $m\ast p$ alternatives, we add $\theta$ to A and some $\{\theta ,b_i=v_j\}$ to B (for $1\le i\le m$, $1\le j\le p$). After such updates, the number of the A-strict or of the B-strict free constants decreases because we added an explicitly defining equation in all cases (see the above remark about ‘term sharing’). Thus, in the end, it will be possible to assert (explicitly or implicitly) an equality or a disequality for every pair of free constants. Since this is precisely the condition for consistency in the combined Nelson–Oppen procedure [42], this cannot happen because we assumed that $A_0\wedge B_0$ was $T_1\cup T_2$-unsatisfiable; hence, every leaf of the tree to be built must contain a contradiction either in the ${\mathsf{\Sigma }}_1$-part or in the ${\mathsf{\Sigma }}_2$-part of its labeling constraint so that an interpolant can be extracted from every leaf.

4. Non-Disjoint Combinations

Whenever signatures are not disjoint, transfer results are harder to obtain. A crucial notion here is $T_0$-compatibility [56], which we are going to introduce in the following. This section is based on the results presented in [37,57].

Recall [41] that a universal theory $T_0$ has a model completion$T_0^{\star }$ iff $T_0^{\star }\supseteq T_0$ is a stronger theory in the same language of $T_0$ such that: (i) Every model of $T_0$ can be embedded into a model of $T_0^{\star }$; and (ii) $T_0^{\star }$ has quantifier elimination. The definition of a model completion could be suitably extended to theories which are not universal, but we do not need to consider this more general case. Alternative equivalent definitions are possible (for instance, condition (ii) is equivalent to the fact that the union of $T_0^{\star }$ and of the diagram of a model of $T_0$ is a complete theory).

Definition 5.

Let T be a theory in the signature Σ and let $T_0$ be a universal theory in a subsignature ${\mathsf{\Sigma }}_0\subseteq \mathsf{\Sigma }$ such that $T_0\subseteq T$. We say that T is$T_0$-compatible iff there is a ${\mathsf{\Sigma }}_0$-theory $T_0^{\star }$ such that:

(i)

$T_0\subseteq T_0^{\star }$;

(ii)

$T_0^{\star }$ is a model completion of $T_0$;

(iii)

Every model of T can be embedded, as a Σ-structure, into a model of $T\cup T_0^{\star }$.

$T_0$-compatibility is a generalization of stable infiniteness; in fact, a theory T is stably infinite iff it is $T_0$-compatible, where $T_0$ is the pure equality theory in the empty signature.

In [56], it is shown that the decidability of the SMT problem transfers from two theories to their non-disjoint combination in case the two theories are both $T_0$-compatible with respect to a locally finite theory in their shared signature (this result has as a special case the transfer of the decidability of the global consequence relations to fusions of modal logics [58]; see below). More results that replace local finiteness with a so-called ‘noetherianity condition’ are given in [59].

Strong Amalgamation over a Horn Theory

In [37], two results are given concerning combined quantifier-free interpolation in the case of non-disjoint signatures. We report the second one only, which is easier to formulate and more effective in the applications.

A $\mathsf{\Sigma }$-theory T is universal Horn iff it can be axiomatized via formulæ of the form $A_1\wedge \cdots \wedge A_n\to B$, where the $A_i$ and B are all atoms(the standard definition of a universal Horn theory would include also the case where B is ⊥, we disregarded this case for simplicity and because our applications to modal logic do not require it). In purely functional signatures, universal Horn theories axiomatize quasi-varieties.

One important fact is that the categories of models of universal Horn theories are co-complete [60]; hence, in particular, pushouts exist.

Definition 6.

Let T be a theory and let $({\mathcal{M}}_1,{\mathcal{M}}_2,\mathcal{A})$ be a T-fork. A pushout of the fork is a triple $(\mathcal{M},{\mu }_1,{\mu }_2)$, where $\mathcal{M}$ is a T-model and ${\mu }_1:{\mathcal{M}}_1⟶\mathcal{M}$, ${\mu }_2:{\mathcal{M}}_2⟶\mathcal{M}$ are Σ-homomorphisms whose restrictions to the support of $\mathcal{A}$ coincide, such that for every other triple $({\mathcal{M}}^{\prime },{\mu }_1^{\prime },{\mu }_2^{\prime })$ with the same properties, there is a unique homomorphism (called the comparison homomorphism) $\theta :\mathcal{M}⟶{\mathcal{M}}^{\prime }$ such that $\theta \circ {\mu }_i={\mu }_i^{\prime }$ ($i=1,2$).

If the pushout $(\mathcal{M},{\mu }_1,{\mu }_2)$ of the T-fork $({\mathcal{M}}_1,{\mathcal{M}}_2,\mathcal{A})$ is a T-amalgam (i.e., if ${\mu }_1,{\mu }_2$ are embeddings), it is called the minimal T-amalgam of the T-fork.

Notice that, even when the pushout is a T-amalgam, comparison morphisms need not be injective. This makes the next definition interesting.

Definition 7.

Let T be a theory in a signature Σ; let $T_0\subseteq T$ be a universal Horn theory in a subsignature ${\mathsf{\Sigma }}_0\subseteq \mathsf{\Sigma }$ with the amalgamation property. We say that T is$T_0$-strongly sub-amalgamable iff every T-fork $({\mathcal{M}}_1,{\mathcal{M}}_2,\mathcal{A})$ has a T-amalgam $\mathcal{M}$ such that the comparison morphism with respect to the minimal $T_0$-amalgam of the ${\mathsf{\Sigma }}_0$-reduct of the T-fork $({\mathcal{M}}_1,{\mathcal{M}}_2,\mathcal{A})$ is injective.

Notice that strong amalgamation is nothing but $T_0$-strong amalgamability, where $T_0$ is the pure equality theory in the empty signature. Thus, the following transfer result is a genuine generalization of Theorem 2:

Theorem 7

[37]. If $T_1,T_2$ are both $T_0$-compatible and $T_0$-strongly sub-amalgamable (for an amalgamable universal Horn theory $T_0$ in their common subsignature ${\mathsf{\Sigma }}_0$), then so is $T_1\cup T_2$.

The above theorem has interesting applications to modal logic. In the following, we let $BA$ be the theory of Boolean algebras. Recall that a Boolean algebra is defined to be a bounded and complemented distributive lattice; since Boolean algebras have a meet-semilattice reduct, it is possible to introduce in them a partial ordering relation $x\le y$ via the definition $x\sqcap y=x$, where ⊓ is the meet operation.. It is well known [41] that $BA$ has a model completion, which is the theory of atomless Boolean algebras: A Boolean algebra is said to be atomless iff it has no non-zero ≤-minimal element.

A BAO-equational theory is any theory T whose signature extends the signature of Boolean algebras and whose axioms are all equations and include the Boolean algebra axioms. BAO stands for ‘Boolean algebras with operations’. BAO-equational theories arise as algebraic semantics of propositional modal logics [61]; for instance, modal algebras (i.e., Boolean algebras endowed with a unary operator □ preserving meets and 1) are Lindenbaum algebras of propositional calculi based on the modal system K. However, we do not assume here any ‘normality’ conditions on the operations of a BAO; hence, BAO are algebraic counterparts of classical modal logics in the sense of [62] (in a classical modal logic, the only assumption made on the modal operators is that the replacement rule for equivalent formulae applies).

The fusion of two BAO-equational theories $T_1$ and $T_2$ is just their combination $T_1\cup T_2$ (when speaking of the fusion of $T_1$ and $T_2$, we assume that $T_1$ and $T_2$ share only the Boolean algebras’ operations and no other symbols). This notion of fusion matches with the standard notion of fusion [58] of the modal logics that are counterparts in propositional logic of the algebraic theories $T_1,T_2$.

Any $BAO$-equational theory T is $BA$-compatible; to see this, it is sufficient to show that a model $\mathcal{M}$ of T embeds into a model ${\mathcal{M}}^{\prime }$ of T whose Boolean reduct is atomless. This is done by taking the colimit of the chain defined as follows: Let ${\mathcal{M}}_0$ be $\mathcal{M}$, let ${\mathcal{M}}_{k+1}$ be ${\mathcal{M}}_k\times {\mathcal{M}}_k$, and use the diagonal maps as embeddings ${\delta }_k:{\mathcal{M}}_k⟶{\mathcal{M}}_{k+1}$.

Thus, in order to apply Theorem 7, we only need to characterize $BA$-strong sub-amalgamability. Surprisingly, this is nothing but a well-known notion from the literature.

Definition 8.

We say that a BAO-equational theory T has the superamalgamation property [63] iff for every T-fork $({\mathcal{M}}_1,{\mathcal{M}}_2,\mathcal{A})$, there exists a T-amalgam $(\mathcal{M},{\mu }_1,{\mu }_2)$ such that for every $a_1\in |{\mathcal{M}}_1|,a_2\in \left|{\mathcal{M}}_2\right|$ such that ${\mu }_1\left(a_1\right)\le {\mu }_2\left(a_2\right)$ there exists $a_0\in \left|\mathcal{A}\right|$ such that $a_1\le a_0$ holds in ${\mathcal{M}}_1$ and $a_0\le a_2$ holds in ${\mathcal{M}}_2$.

Theorem 8

[37]. A BAO-equational theory T has the superamalgamation property iff it is $BA$-strongly amalgamable.

As is well known from [63], the superamalgamation property for varieties of modal algebras, in the case of normal modal logics, corresponds to (the local deducibility version of) the Craig interpolation theorem. Thus, Theorem 8 implies, in particular, a Wolter fusion transfer result [58] of the Craig interpolation theorem for normal modal logics. For non-normal modal logics, superamalgamation corresponds to a strong version of the Craig interpolation theorem (encompassing both the local and the global deducibility versions of it) called the comprehensive interpolation property in [37]. Theorem 8 above implies that this comprehensive interpolation property transfers to fusions in the non-normal case, too, as proved in [37].

5. Uniform Interpolants

This section presents results contained in [31,32,38,39,40,64,65]. First, we analyze a strong form of of quantifier-free interpolation and its relationship with model-completeness [31,32]; we then show that, for convex theories, the same hypotheses allowing the transfer of the existence of ordinary interpolants also allow the transfer of the existence of these stronger interpolants [39,40].

Fix a theory T and an existential formula $\exists \underline{e}\varphi (\underline{e},\underline{y})$; a quantifier-free formula $\theta \left(\underline{y}\right)$ is said to be a T-cover [30] (or, simply, a cover) of $\exists \underline{e}\varphi (\underline{e},\underline{y})$ iff the following two conditions are satisfied: (i) $T\vDash \exists \underline{e}\varphi (\underline{e},\underline{y})\to \theta \left(\underline{y}\right)$; (ii) For every formula $\psi (\underline{y},\underline{z})$ such that $T\vDash \exists \underline{e}\varphi (\underline{e},\underline{y})\to \psi (\underline{y},\underline{z})$, we have that $T\vDash \theta \left(\underline{y}\right)\to \psi (\underline{y},\underline{z})$. Sometimes, the cover $\theta \left(\underline{y}\right)$ (which is unique up to T-equivalence) is called a (quantifier-free) uniform interpolant. The reason for this terminalogy comes from the fact that an entailment like $T\vDash \varphi (\underline{e},\underline{y})\to \psi (\underline{y},\underline{z})$ is equivalent (by the standard rule for existential quantifier introduction) to $T\vDash \exists \underline{e}\varphi (\underline{e},\underline{y})\to \psi (\underline{y},\underline{z})$, hence it is immediately seen that a cover $\theta \left(\underline{y}\right)$ of $\exists \underline{e}\varphi (\underline{e},\underline{y})$ can work as an interpolant for all entailments $T\vDash \varphi (\underline{e},\underline{y})\to \psi (\underline{y},\underline{z})$ (varying all $\psi (\underline{y},\underline{z})$ for which the entailment holds).

We say that a theory T has uniform quantifier-free interpolation iff every existential formula $\exists \underline{e}\varphi (\underline{e},\underline{y})$ (equivalently, every primitive formula $\exists \underline{e}\varphi (\underline{e},\underline{y})$) has a T-cover.

The following lemma supplies a semantic counterpart to the notion of a cover. What the lemma essentially says is that the cover of $\exists \underline{e}\varphi (\underline{e},\underline{y})$ expresses a ‘solvability condition’ for $\varphi (\underline{e},\underline{y})$ (seen as a kind of system of equations in the parameters $\underline{y}$); if this solvability condition is true, then it is possible to build (maybe in an extended model) a solution for $\varphi (\underline{e},\underline{y})$ and vice versa.

Lemma 1

[31,32]. A formula $\psi \left(\underline{y}\right)$ is a T-cover of $\exists \underline{e}\varphi (\underline{e},\underline{y})$ iff it satisfies the following two conditions:

(i)

$T\vDash \forall \underline{y}(\exists \underline{e}\varphi (\underline{e},\underline{y})\to \psi \left(\underline{y}\right))$;

(ii)

For every model $\mathcal{M}$ of T and for every tuple of elements $\underline{a}$ from the support of $\mathcal{M}$ such that $\mathcal{M}\vDash \psi \left(\underline{a}\right)$, it is possible to find another model $\mathcal{N}$ of T such that $\mathcal{M}$ embeds into $\mathcal{N}$ and $\mathcal{N}\vDash \exists \underline{e}\varphi (\underline{e},\underline{a})$.

In Section 4, we mentioned the model completion $T^{\star }$ of a universal theory T; we recall from [41] that $T^{\star }$ axiomatizes the models of T that are existentially closed for T, i.e., those models $\mathcal{M}$ of T for which an existential formula with parameters in $\left|\mathcal{M}\right|$ having a solution in an extension of $\mathcal{M}$, which is also a model of T, has a solution in $\mathcal{M}$ itself. If a theory has uniform interpolation, then every existential formula $\exists \underline{e}\varphi (\underline{e},\underline{y})$ has a T-cover, so it is possible to express the solvability condition of $\varphi (\underline{e},\underline{y})$ via the cover. In this way, we can axiomatize existentially closed models; we just say that ‘whatever is solvable actually has a solution’. These intuitive considerations show why the following result comes with no surprise.

Theorem 9

[31,32,66]. Suppose that T is a universal theory. Then, T has a model completion $T^{\star }$ iff T has uniform quantifier-free interpolation. If this happens, $T^{\star }$ is axiomatized by the infinitely many sentences

$$\forall \underline{y}(\psi \left(\underline{y}\right)\to \exists \underline{e}\varphi (\underline{e},\underline{y}))$$

(19)

where $\exists \underline{e}\varphi (\underline{e},\underline{y})$ is an existential formula and ψ is a T-cover of it.

5.1. Uniform Interpolants in $\mathcal{EUF}$

Whereas it is clear that theories enjoying quantifier elimination also have uniform interpolation, it is less evident whether other theories used in verification have covers or not. $\mathcal{EUF}$ is the typical theory used in verification that is not a theory axiomatizing arithmetic data and that does not enjoy quantifier elimination. That is why investigating uniform interpolation in $\mathcal{EUF}$ can be interesting. In fact, $\mathcal{EUF}$ does enjoy uniform interpolation; the result was stated on various occasions in the literature (including, e.g., [30]), but the first proofs were only published in the conference paper [31] and its journal version [32]. Alternative proofs are reported in [38,65]. Actually, these papers contain three different algorithms for computing uniform interpolants in $\mathcal{EUF}$. In this subsection, we only report the first algorithm from [38,64,65], which is the simplest one to explain.

The algorithm is based on transformation rules. We first need some definitions (for simplicity, we assume that the signature is functional).

A flat literal is a literal included in the following list:

$$f(a_1,\cdots ,a_n)=b,a_1=a_2,a_1\ne a_2$$

(20)

where $a_1,\cdots ,a_n$ and b are (not necessarily distinct) variables or constants. A formula is flat iff all literals occurring in it are flat; flat terms are terms occurring in the literals listed above in (20).

An explicit definition via a directed acyclic graph (abbreviated as a DAG-definition, or simply as a DAG) is any formula $\mathtt{ExplDef}(\underline{y},\underline{z})$ of the following form (where $\underline{y}:=y_1\cdots ,y_n$):

$$\underset{i=1}{\overset{n}{\bigwedge }}(y_i=f_i(y_1,\cdots ,y_{i-1},\underline{z})).$$

Thus, $\mathtt{ExplDef}(\underline{y},\underline{z})$ provides an explicit definition of the $\underline{y}$ in terms of the parameters $\underline{z}$. Given such a DAG-definition $\mathtt{ExplDef}(\underline{y},\underline{z})$, we can, in fact, associate to it a substitution $\sigma$ so that a formula such as

$$\exists \underline{y}(\mathtt{ExplDef}(\underline{y},\underline{z})\wedge \Phi (\underline{y},\underline{z}))$$

(21)

is equivalent to $\Phi (\sigma \left(\underline{y}\right),\underline{z})$. The formula $\Phi (\sigma \left(\underline{y}\right),\underline{z})$ is said to be the unravelling of (21); notice that computing such an unravelling by explicitly performing the required substitutions causes an exponential blow-up.

We want to compute the cover of a primitive formula $\exists \underline{e}\varphi (\underline{e},\underline{z})$; we can assume without loss of generality that the constraint $\varphi (\underline{e},\underline{z})$ is flat. To see this, it is sufficient to apply (as a pre-processing step) the well-known Congruence Closure Transformations, as explained, e.g., in [67] (these transformations have a linear cost).

The algorithm manipulates formulae in the following format:

$$\exists \underline{y}(\mathtt{ExplDef}(\underline{y},\underline{z})\wedge \Phi (\underline{y},\underline{z})\wedge \exists \underline{e}\mathsf{\Psi }(\underline{e},\underline{y},\underline{z}))$$

(22)

where $\mathtt{ExplDef}(\underline{y},\underline{z})$ is a DAG and $\Phi ,\mathsf{\Psi }$ are flat constraints (notice that the $\underline{e}$ do not occur in $\Phi$). When writing formulae such as (22), we usually omit the existential quantifiers $\exists \underline{y}$ and $\exists \underline{e}$ for brevity.

Initially, $\mathtt{ExplDef}$ and $\Phi$ are the empty conjunction. In (22), the variables $\underline{z}$ are called parameter variables, the variables $\underline{y}$ are called (explicitly) defined variables, and the variables $\underline{e}$ are called (truly) quantified variables. The algorithm does not modify the variables $\underline{z}$; on the other hand, it might cause some quantified variable to disappear or to be renamed as a defined variable. Below, the letters $a,b,\cdots$ range over $\underline{e}\cup \underline{y}\cup \underline{z}$.

Definition 9.

A term t (or a literal L) is $\underline{e}$-free when there is no occurrence of any of the variables $\underline{e}$ in t (or in L). Two flat terms $t,u$ of the kinds

$$t:=f(a_1,\cdots ,a_n)u:=f(b_1,\cdots ,b_n)$$

(23)

are said to be compatible iff, for every $i=1,\cdots ,n$, either $a_i$ is identical to $b_i$ or both $a_i$ and $b_i$ are $\underline{e}$-free. The difference set of two compatible terms as above is the set of disequalities $a_i\ne b_i$, where $a_i$ is not identical to $b_i$.

The algorithm (taken from [38,64,65]) applies the rules below in any order, except the last one, which has lower priority. The last rule splits the execution of the algorithm into several branches; each branch will produce a different disjunct in the output formula.

(1)

Simplification Rules:

(1.0)

If an atom such as $t=t$ belongs to $\mathsf{\Psi }$, just remove it; if a literal such as $t\ne t$ occurs somewhere, delete $\mathsf{\Psi }$, replace $\Phi$ with ⊥, and stop;

(1.i)

If t is not a variable and $\mathsf{\Psi }$ contains both $t=a$ and $t=b$, remove the former and replace it with $a=b$.

(1.ii)

If $\mathsf{\Psi }$ contains $e_i=e_j$ with $i>j$, remove it and replace $e_i$ with $e_j$ everywhere.

(2)

DAG Update Rule: If $\mathsf{\Psi }$ contains $e_i=t(\underline{y},\underline{z})$, remove it, rename $e_i$ as $y_j$ everywhere (for fresh $y_j$), and add $y_j=t(\underline{y},\underline{z})$ to $\mathtt{ExplDef}(\underline{y},\underline{z}).$ More formally:

$$\mathtt{ExplDef}(\underline{y},\underline{z})\wedge \Phi (\underline{y},\underline{z})\wedge \left(\mathsf{\Psi }(\underline{e},e_i,\underline{y},\underline{z})\wedge e_i=t(\underline{y},\underline{z})\right)$$

$$\left(\mathtt{ExplDef}(\underline{y},\underline{z})\wedge y_j=t(\underline{y},\underline{z})\right)\wedge \Phi (\underline{y},\underline{z})\wedge \mathsf{\Psi }(\underline{e},y_j,\underline{y},\underline{z})$$

(3)

$\underline{e}$-Free Literal Rule: If $\mathsf{\Psi }$ contains a literal $L(\underline{y},\underline{z})$, move it to $\Phi (\underline{y},\underline{z})$. More formally:

$$\mathtt{ExplDef}(\underline{y},\underline{z})\wedge \Phi (\underline{y},\underline{z})\wedge \left(\mathsf{\Psi }(\underline{e},\underline{y},\underline{z})\wedge L(\underline{y},\underline{z})\right)$$

$$\mathtt{ExplDef}(\underline{y},\underline{z})\wedge \left(\Phi (\underline{y},\underline{z})\wedge L(\underline{y},\underline{z})\right)\wedge \mathsf{\Psi }(\underline{e},\underline{y},\underline{z})$$

(4)

Splitting Rule: If $\mathsf{\Psi }$ contains a pair of atoms $t=a$ and $u=b$, where t and u are compatible flat terms as in (23) (thus, in particular, t and u are of the kinds $f(a_1,\cdots ,a_n)$ and $f(b_1,\cdots ,b_n)$, respectively), and no disequality from the difference set of $t,u$ belongs to $\Phi$, then apply one of the following alternatives:

(4.0)

Remove from $\mathsf{\Psi }$ the atom $f(b_1,\cdots ,b_n)=b$, add to $\mathsf{\Psi }$ the atom $a=b$, and add to $\Phi$ all equalities $a_i=b_i$ such that $a_i\ne b_i$ is in the difference set of $t,u$;

(4.1)

Add to $\Phi$ one of the disequalities from the difference set of $t,u$ (notice that the difference set cannot be empty; otherwise, Rule (1.i) applies).

Theorem 10

[38,64,65]. Suppose that we apply the above algorithm to the primitive formula $\exists \underline{e}\left(\varphi (\underline{e},\underline{z})\right)$ and that the algorithm terminates with its branches in the states

$${\mathtt{ExplDef}}_1(\underline{y},\underline{z})\wedge {\Phi }_1({\underline{y}}_1,\underline{z})\wedge {\mathsf{\Psi }}_1({\underline{e}}_1,{\underline{y}}_1,\underline{z}),\cdots ,{\mathtt{ExplDef}}_k(\underline{y},\underline{z})\wedge {\Phi }_k({\underline{y}}_k,\underline{z})\wedge {\mathsf{\Psi }}_k({\underline{e}}_k,{\underline{y}}_k,\underline{z})$$

Then, the cover of $\exists \underline{e}\left(\varphi (\underline{e},\underline{z})\right)$ in $\mathcal{EUF}$ is the disjunction of the unravellings of the formulæ

$$\exists {\underline{y}}_i({\mathtt{ExplDef}}_i(\underline{y},\underline{z})\wedge {\Phi }_i({\underline{y}}_i,\underline{z}))$$

(24)

while varying $i=1,\cdots ,k$.

The proof (shown in [38,65]) is based on Lemma 1 and essentially shows that if we conjoin the Robinson Diagram of a model satisfying ${\mathtt{ExplDef}}_i(\underline{y},\underline{z})\wedge {\Phi }_i({\underline{y}}_i,\underline{z})$ (relatively to a certain assignment to the variables ${\underline{y}}_i,\underline{z}$) with ${\mathsf{\Psi }}_i({\underline{e}}_i,{\underline{y}}_i,\underline{z})$, we get a canonical rewrite system (under a suitable reduction ordering; see [68] for information on rewrite systems).

Example 6.

This example is analyzed in [38,64,65]. Let us compute a cover of the formula $\exists e_0(g(z_4,e_0)=z_0\wedge f(z_2,e_0)=g(z_3,e_0)\wedge h\left(f(z_1,e_0)\right)=z_0)$. We first need to flatten it; this produces the set of literals

$$g(z_4,e_0)=z_0\wedge e_1=f(z_2,e_0)\wedge e_1=g(z_3,e_0)\wedge e_2=f(z_1,e_0)\wedge h\left(e_2\right)=z_0$$

(25)

where we have two newly introduced variables $e_1,e_2$ to be eliminated, too. After applying Splitting (4.0), the equality $g(z_3,e_0)=e_1$ is removed and the new equalities $z_3=z_4$, $e_1=z_0$ are introduced. Now, (2) renames $e_1$ as $y_1$ by (2). We apply (4.0) again; this removes $f(z_1,e_0)=e_2$ and adds the equalities $z_1=z_2$, $e_2=y_1$; moreover, the variable $e_2$ is renamed as $y_2$. We can now apply (3) to the literal $h\left(y_2\right)=z_0$. The branch terminates with $y_1=z_0\wedge y_2=y_1\wedge z_1=z_2\wedge z_3=z_4\wedge h\left(y_2\right)=z_0\wedge f(z_2,e_0)=y_1\wedge g(z_4,e_0)=z_0$. This gives $z_1=z_2\wedge z_3=z_4\wedge h\left(z_0\right)=z_0$ as a first disjunct of the uniform interpolant. The other branches give $z_1=z_2\wedge z_3\ne z_4$, $z_1\ne z_2\wedge z_3=z_4$, and $z_1\ne z_2\wedge z_3\ne z_4$ as further disjuncts, so that our cover turns out to be logically equivalent to $z_1=z_2\wedge z_3=z_4\to h\left(z_0\right)=z_0$.

The above algorithm has exponential complexity (the branches have quadratic size); notice, however, that, if the signature only contains unary function symbols, there is no need to apply the Splitting Rule, and hence, the complexity is polynomial; the case of a signature with only unary function symbols is important in the applications to data-aware verification because it allows the formalization of read-only databases with primary and foreign keys [35].

5.2. Combined Uniform Interpolants

We now investigate combined uniform interpolants by starting from the convex case and by showing the algorithm presented in [39,40]. Let us fix a convex, stably infinite, equality-interpolating universal theory admitting a model completion. Let T be such a theory, let $\mathsf{\Sigma }$ be its signature, and let $T^{\star }$ be its model completion. Consider a conjunction of $\mathsf{\Sigma }$-literals $\varphi (\underline{x},\underline{y})$, where $\underline{y}=y_1,\cdots ,y_n$ (recall that the tuple $\underline{x}$ is disjoint from the tuple $\underline{y}$ according to the conventions from Section 2).

For $i=1,\cdots ,n$, we let the formula ${\mathtt{ImplDef}}_{\varphi ,y_i}^T\left(\underline{x}\right)$ be the quantifier-free formula equivalent in $T^{\star }$ to the formula

$$\forall \underline{y}\forall {\underline{y}}^{\prime }(\varphi (\underline{x},\underline{y})\wedge \varphi (\underline{x},{\underline{y}}^{\prime })\to y_i=y_i^{\prime })$$

(26)

where the ${\underline{y}}^{\prime }$ are renamed copies of the $\underline{y}$. The following lemma (taken from [39,40]) comes from the primitive Beth definability property (recall the paragraph following Proposition 1):.

Lemma 2.

Let $L_{i1}\left(\underline{x}\right)\vee \cdots \vee L_{i{k}_i}\left(\underline{x}\right)$ be the disjunctive normal form (DNF) of ${\mathtt{ImplDef}}_{\varphi ,y_i}^T\left(\underline{x}\right)$. Then, for every $j=1,\cdots ,k_i$, there is a $\mathsf{\Sigma }\left(\underline{x}\right)$-term $t_{ij}\left(\underline{x}\right)$ such that

$$T⊢L_{ij}\left(\underline{x}\right)\wedge \varphi (\underline{x},\underline{y})\to y_i=t_{ij}.$$

(27)

The above lemma is the key technical ingredient for the proof of the following result.

Theorem 11

[39,40]. Let $T_1,T_2$ be convex, stably infinite, equality-interpolating, universal theories over disjoint signatures with uniform quantifier-free interpolation. Then, $T_1\cup T_2$ has uniform quantifier-free interpolation.

We now present the algorithm from [39,40] to compute covers in $T_1\cup T_2$ when the hypotheses of the above theorem are satisfied and the $SMT\left(T_1\right),SMT\left(T_2\right)$ satisfiability problems are decidable. We show how compute the cover of a primitive formula $\exists \underline{e}\varphi (\underline{e},\underline{z})$, where we freely assume that the literals in $\varphi$ are all flat: if we let ${\mathsf{\Sigma }}_1$ to be the signature of $T_1$ and ${\mathsf{\Sigma }}_2$ to be the signature of $T_2$, flatness means in particular that such literals are either ${\mathsf{\Sigma }}_1$-literals or ${\mathsf{\Sigma }}_2$-literals or both (the latter can obviously be the case only for equalities or negated equalities involving variables). The idea behind the algorithm is that the input cover algorithms can be separately applied, once all potential definability phenomena have been identified.

A working formula is a formula of the kind

$$\exists \underline{z}(\mathtt{ExplDef}(\underline{z},\underline{x})\wedge \exists \underline{e}({\psi }_1(\underline{x},\underline{z},\underline{e})\wedge {\psi }_2(\underline{x},\underline{z},\underline{e}))),$$

(28)

where $\mathtt{ExplDef}(\underline{z},\underline{x})$ is a DAG, ${\psi }_1$ is a conjunction of ${\mathsf{\Sigma }}_1$-literals, and ${\psi }_2$ is a conjunction of ${\mathsf{\Sigma }}_2$-literals. We assume that ${\psi }_1,{\psi }_2$ in a working formula (28) always contain the literals $e_i\ne e_j$ (for distinct $e_i,e_j$ from $\underline{e}$) as a conjunct; this can be forced at the initialization stage by making a case-split followed by replacements of equals by equals. Contrary to what we did in the $\mathcal{EUF}$ case above, here, we do not need to separate the literals that do not contain the truly existential variables $\underline{e}$ from the other ones.

A working formula such as (28) is said to be terminal iff, for every existential variable $e_i\in \underline{e}$, we have that

$$T_1⊢{\psi }_1\to \neg {\mathtt{ImplDef}}_{{\psi }_1,e_i}^{T_1}(\underline{x},\underline{z})\mathrm{and}{T}_2⊢{\psi }_2\to \neg {\mathtt{ImplDef}}_{{\psi }_2,e_i}^{T_2}(\underline{x},\underline{z}).$$

(29)

Intuitively, in a terminal working formula, all variables that are not parameters are either explicitly definable or recognized not to be implicitly definable by both theories. Notice that the validity tests for the implications (29) can be effectively discharged using the quantifier-free satisfiability procedures in $T_1,T_2$.

We first observe (see [39,40] for details) that every working formula is equivalent (modulo $T_1\cup T_2$) to a disjunction of terminal working formulæ. Such a disjunction of terminal working formulæ can be computed as follows: One exhaustively applies the following transformations in all possible ways (the output is the disjunction of the different outcomes).

(1)

Update ${\psi }_1$ by adding to it a disjunct from the DNF of ${\bigwedge }_{e_i\in \underline{e}}\neg {\mathtt{ImplDef}}_{{\psi }_1,e_i}^{T_1}(\underline{x},\underline{z})$ and ${\psi }_2$ by adding to it a disjunct from the DNF of ${\bigwedge }_{e_i\in \underline{e}}\neg {\mathtt{ImplDef}}_{{\psi }_2,e_i}^{T_2}(\underline{x},\underline{z})$;

(2.i)

Select $e_i\in \underline{e}$ and $h\in \{1,2\}$; then, update ${\psi }_h$ by adding to it a disjunct $L_{ij}$ from the DNF of ${\mathtt{ImplDef}}_{{\psi }_h,e_i}^{T_h}(\underline{x},\underline{z})$; the equality $e_i=t_{ij}$ (where $t_{ij}$ is the term mentioned in Lemma 2) is added to $\mathtt{ExplDef}(\underline{z},\underline{x})$; the variable $e_i$ becomes, in this way, part of the defined variables.

To conclude, we need the final fact (again, shown in [39,40]) that the cover of a working Formula (28) that is terminal is given by the unravelling of the explicit definitions of the variables $\underline{z}$ from the formula

$$\exists \underline{z}(\mathtt{ExplDef}(\underline{z},\underline{x})\wedge {\theta }_1(\underline{x},\underline{z})\wedge {\theta }_2(\underline{x},\underline{z}))$$

(30)

where ${\theta }_1(\underline{x},\underline{z})$ is the $T_1$-cover of $\exists \underline{e}{\psi }_1(\underline{x},\underline{z},\underline{e})$ and ${\theta }_2(\underline{x},\underline{z})$ is the $T_2$-cover of $\exists \underline{e}{\psi }_2(\underline{x},\underline{z},\underline{e})$.

A remarkable corollary of the above theorem says that existence of uniform interpolants is preserved when adding free function symbols to a convex, stably infinite, equality-interpolating, universal theory with uniform interpolants (this is because the combination with $\mathcal{EUF}$ enjoys the hypotheses of Theorem 11). Unfortunately, the convexity hypothesis is indispensable for this result to hold, as the following counterexample from [39,40] shows.

We take as $T_1$ the integer difference logic $\mathcal{IDL}$ of Example 2; notice that this theory is stably infinite, universal, and has quantifier elimination (thus, it coincides with its own model completion). This theory is not convex; however, it is equality interpolating, as seen in Section 3 above. As $T_2$, we take $\mathcal{EUF}\left({\mathsf{\Sigma }}_f\right)$, where ${\mathsf{\Sigma }}_f$ has just one unary free function symbol f (this f is supposed not to belong to the signature of $T_1$).

Proposition 2

[39,40]. Let $T_1,T_2$ be as above; the formula

$$\exists e(0<e\wedge e<x\wedge f(e)=0)$$

(31)

does not have a cover in $T_1\cup T_2$.

The counterexample still applies when replacing integer difference logic with linear integer arithmetics.

6. Conclusions

We investigated transfer results concerning the existence of quantifier-free (ordinary and uniform) interpolants to combined first-order theories. The investigation used semantic and model-theoretic tools in an essential way in order to obtain appropriate conceptualizations for justifying concrete algorithms.

Some problems are left open; in particular, the results concerning the case of non-disjoint signatures are far from being exhaustive. Indeed, in the case of non-disjoint signatures, sufficient conditions for the transfer of uniform interpolants are completely missing.

Advanced combination problems tend to be rather difficult in nature; however, very often, applications show unexpectedly interesting research perspectives that are worth pursuing. For instance, in [40], a strong result (working only under the stable infiniteness hypothesis) for the transfer of existence of uniform interpolants is obtained in the case of special many-sorted disjoint signature combinations (called ‘tame combinations’) arising in the area of verification of data-aware processes [34,35,69].

Applications are also important for testing the feasibility of the algorithms suggested by theoretical research in concrete implementations. As briefly mentioned in the introduction, frameworks for the verification of data-aware processes [35,69,70] provide a particularly interesting setting where (combined) uniform interpolation plays a crucial role from the theoretical, the methodological/algorithmic, and the operational perspectives (see [71] for an exhaustive introduction to this topic). In this context, complex dynamic systems that can interact with a persistent data storage are verified against some property of interest via sophisticated techniques based on SMT-solving and on automated reasoning; specifically, the presence of the ‘data’ component, which is usually represented as relational databases that the ‘process’ component can query and update, requires the development of suitable techniques for eliminating (to some extent) quantifiers binding variables that range over the content of such databases. This task can be effectively and efficiently performed by computing (combined) uniform interpolants [31,32,39,40]. This motivated the implementation of algorithms for computing combined uniform interpolants in the state-of-the-art MCMT model checker [72]. We demonstrated the feasibility of this approach in [71] by testing MCMT against a benchmark of concrete data-aware processes, and we showed in [69,70,71,73,74] how these techniques turn out to be extremely useful for developing operational verification frameworks for modeling and verifying business processes enriched with concrete data that emerge in real-world scenarios and in business process management [75] within contemporary organizations.