Open Access 12052022
Combination of Uniform Interpolants via Beth Definability
Published in: Journal of Automated Reasoning  Issue 3/2022
Abstract
Uniform interpolants were largely studied in nonclassical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifierfree interpolants (sometimes referred to as “covers”) in firstorder theories. In this paper, we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that, for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis needed to transfer quantifierfree interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. In the nonconvex case, we show by a counterexample that covers may not exist in the combined theories, even in case combined quantifierfree interpolants do exist. However, we exhibit a cover transfer algorithm operating also in the nonconvex case for special kinds of theory combinations; these combinations (called ‘tame combinations’) concern multisorted theories arising in many modelchecking applications (in particular, the ones oriented to verification of dataaware processes).
1 Introduction
This paper is devoted to combination results concerning uniform interpolants. In this introduction, we summarize the two main (quite independant indeed) research lines that investigated uniform interpolants in the last three decades. We first recall what uniform interpolants are; we fix a logic or a theory T and a suitable fragment (propositional, firstorder quantifierfree, etc.) of its language L. Given an Lformula \(\phi ({\underline{x}}, {\underline{y}})\) (here \({\underline{x}},{\underline{y}}\) are the variables occurring in \(\phi \)), a uniform interpolant of \(\phi \) (w.r.t. \({\underline{y}}\)) is an Lformula \(\phi '({\underline{x}})\) where only the \({\underline{x}}\) occur, and that satisfies the following two properties: (i) \(\phi ({\underline{x}}, {\underline{y}})\vdash _T \phi '({\underline{x}})\); (ii) for any further Lformula \(\psi ({\underline{x}}, {\underline{z}})\) such that \(\phi ({\underline{x}}, {\underline{y}}) \vdash _T \psi ({\underline{x}}, {\underline{z}})\), we have \(\phi '({\underline{x}}) \vdash _T \psi ({\underline{x}}, {\underline{z}})\). Whenever uniform interpolants exist, one can compute an interpolant for an entailment like \(\phi ({\underline{x}}, {\underline{y}}) \vdash _T \psi ({\underline{x}}, {\underline{z}})\) in a way that is independent of \(\psi \).
Uniform interpolants were originally studied in the context of nonclassical logics, starting from the pioneering work by Pitts [40]. Uniform interpolants have in such nonclassical logics context a ‘local’ and a ’global’ version, depending on how the entailment \(\vdash _T\) is interpreted: in the local version it is interpreted as ‘provability of implication’, whereas in the global version is interpreted as ‘provability under assumption’ (the two versions coincide for intuitionistic logic, but not for modal logics). The local version of uniform interpolation allows an (albeit not faithful) interpretation of the second order propositional calculus into plain propositional calculus, whereas the global version can be used in the axiomatization of model completions for the corresponding classes of algebras (see below). Uniform interpolants can be sematically connected to some appropriate notion of bisimulation at the level of Kripke models [13].
Advertisement
The existence of uniform interpolants is an exceptional phenomenon, which is however not so infrequent, as witnessed by a large literature in nonclassical logics (a nonexhaustive list includes [1, 16, 22, 23, 25, 34, 37, 42, 45, 46]). The main results from the above papers are that uniform interpolants exist for intuitionistic logic and for some modal systems (like the GödelLöb system and the S4.Grz system); they do not exist for instance in S4 and K4, whereas for the basic modal system K they exist for the local version but not for the global version (the opposite situation is also wellpossible, already in the locally finite case, as a consequence of Maksimova’s results on amalgamation and superamalgamation [35, 36]). The connection between (global) uniform interpolants and model completions (for equational theories axiomatizing the varieties corresponding to propositional logics) was first stated in [24] and further developed in [25, 34, 37, 45].
In the last decade, also the automated reasoning community developed an increasing interest in uniform interpolants, with particular focus on quantifierfree fragments of firstorder theories. This is witnessed by various talks and drafts by D. Kapur presented in many conferences and workshops (FloC 2010, ISCAS 201314, SCS 2017 [33]), as well as by the paper [32] by Gulwani and Musuvathi in ESOP 2008. In this last paper uniform interpolants were renamed as covers, a terminology we shall frequently adopt in this paper too. In these contributions, examples of cover computations were supplied and also some algorithms were sketched. The first formal proof about existence of covers in \(\mathcal {EUF}\) was however published by the present authors only in [6]; such a proof was equipped with powerful semantic tools (the CoverbyExtensions Lemma 1 below) coming from the connection to modelcompleteness, as well as with an algorithm relying on a constrained variant of the Superposition Calculus (two simpler algorithms are studied in [27], the related completeness proofs are available in [26, 30]). The usefulness of covers in model checking was already stressed in [32] and further motivated by our recent line of research on the verification of dataaware processes [4, 5, 7, 9]. Notably, it is also operationally mirrored in the MCMT [21] implementation since version 2.8. Covers (via quantifier elimination in model completions and hierarchical reasoning) play an important role in symbol elimination problems in theory extensions, as witnesssed in the comprehensive paper [43] and in related papers [39] studying invariant synthesis in model checking applications.
An important question suggested by the applications is the cover transfer problem for combined theories: for instance, when modeling and verifying dataaware processes, it is natural to consider the combination of different theories, such as the theories accounting for the readwrite and readonly data storage of the process as well as those for the elements stored therein [5‐7, 10]. Formally, the cover transfer problem can be stated as follows: by supposing that covers exist in theories \(T_1, T_2\), under which conditions do they exist also in the combined theory \(T_1\cup T_2\)? In this paper we show that the answer is affirmative in the disjoint signatures convex case, using the same hypothesis (that is, the equality interpolating condition) under which quantifierfree interpolation transfers. Thus, for convex theories we essentially obtain a necessary and sufficient condition, in the precise sense captured by Theorem 6 below. We also prove that if convexity does not hold (as it happens, e.g., for integer difference logic \(\mathcal {IDL}\) or for linear integer arithmetics \(\mathcal {LIA} \)), the nonconvex equality interpolating property [2] may not be sufficient to ensure the cover transfer property. As a witness for this, we show that \(\mathcal {EUF}\) combined with integer difference logic or with linear integer arithmetics constitutes a counterexample.
The main tool employed in our combination result is the Beth definability theorem for primitive formulae (this theorem has been shown to be equivalent to the equality interpolating condition in [2]). In order to design a combined cover algorithm, we exploit the equivalence between implicit and explicit definability that is supplied by the Beth theorem. Implicit definability is reformulated, via covers for input theories, at the quantifierfree level. Thus, the combined cover algorithm guesses the implicitly definable variables, then eliminates them via explicit definability, and finally uses the componentwise input cover algorithms to eliminate the remaining (non implicitly definable) variables. The identification and the elimination of the implicitly defined variables via explicitly defining terms is an essential step towards the correctness of the combined cover algorithm: when computing a cover of a formula \(\phi ({\underline{x}}, {\underline{y}})\) (w.r.t. \({\underline{y}}\)), the variables \({\underline{x}}\) are (noneliminable) parameters, and those variables among the \({\underline{y}}\) that are implicitly definable need to be discovered and treated in the same way as the parameters \({\underline{x}}\). Only after this preliminary step (Lemma 6 below), the input cover algorithms can be suitably exploited (Proposition 2 below).
Advertisement
The combination result we obtain is quite strong, as it is a typical ‘black box’ combination result: it applies not only to theories used in verification (like the combination of real arithmetics with \(\mathcal {EUF}\)), but also in other contexts. For instance, since the theory \({\mathcal {B}}\) of Boolean algebras satisfies our hypotheses (being model completable and strongly amalgamable [19]), we get that uniform interpolants exist in the combination of \({\mathcal {B}}\) with \(\mathcal {EUF}\). The latter is the equational theory algebraizing the basic nonnormal classical modal logic system \(\mathbf{E}\) from [41] (extended to nary modalities). Notice that this result must be contrasted with the case of many systems of Boolean algebras with operators where existence of uniform interpolation fails [34] (recall that operators on a Boolean algebra are not just arbitrary functions, but are required to be monotonic and also to preserve either joins or meets in each coordinate).
As a last important comment on related work, it is worth mentioning that Gulwani and Musuvathi in [32] also have a combined cover algorithm for some convex, signature disjoint theories. Their algorithm looks quite different from ours; apart from the fact that a full correctness and completeness proof for such an algorithm has never been published, we underline that our algorithm is rooted on different hypotheses. In fact, we only need the equality interpolating condition and we show that this hypothesis is not only sufficient, but also necessary for cover transfer in convex theories; consequently, our result is formally stronger. The equality interpolating condition was known to the authors of [32] (but not even mentioned in their paper [32]): in fact, it was introduced by one of them some years before [47]. The equality interpolating condition was then extended to the non convex case in [2], where it was also semantically characterized via the strong amalgamation property.
The paper is organized as follows: after some preliminaries in Section 2, the crucial CoversbyExtensions Lemma and the relationship between covers and model completions from [6] are recalled in Sect. 3. In Sect. 4, we present some preliminary results from the literature on interpolation, amalgamation, strong amalgamation and Beth definability that are instrumental to our machinery. After some useful facts about convex theories in Sect. 5, we introduce the combined cover algorithms for the convex case and we prove its correctness in Sect. 6; we also present a detailed example of application of the combined algorithm in case of the combination of \(\mathcal {EUF}\) with linear real arithmetic, and we show that the equality interpolating condition is, in a natural sense, necessary for combining covers. In Sect. 7 we exhibit a counterexample to the existence of combined covers in the nonconvex case. Finally, in Sect. 8 we prove that for the ‘tame’ multisorted theory combinations used in our applications to dataaware processes verification, covers existence transfers to the combined theory under only the stable infiniteness requirement for the shared sorts. Section 9 is devoted to the conclusions and discussion of future work. The current paper is the extended version of [8]; in addition to supplying full selfcontained proofs of the results of [8], it contains the entirely new Sect. 8 dedicated to the positive results for the nonconvex tame case.
2 Preliminaries
We adopt the usual firstorder syntactic notions of signature, term, atom, (ground) formula, and so on; our signatures are always finite or countable and include equality. To avoid considering limit cases, we assume that signatures always contain at least an individual constant. We compactly represent a tuple \(\langle x_1,\ldots ,x_n\rangle \) of variables as \({\underline{x}}\); by abuse of notation, we sometimes use \(\langle x_1,\ldots ,x_n\rangle \) to denote also sets of variables (not just tuples). The notation \(t({\underline{x}}), \phi ({\underline{x}})\) means that the term t, the formula \(\phi \) has free variables included in the tuple \({\underline{x}}\). This tuple is assumed to be formed by distinct variables, thus we underline that when we write e.g. \(\phi ({\underline{x}}, {\underline{y}})\), we mean that the tuples \({\underline{x}}, {\underline{y}}\) are made of distinct variables that are also disjoint from each other.
A formula is said to be universal (resp., existential) if it has the form \(\forall {\underline{x}}(\phi ({\underline{x}}))\) (resp., \(\exists {\underline{x}}(\phi ({\underline{x}}))\)), where \(\phi \) is quantifierfree. Formulae with no free variables are called sentences. On the semantic side, we use the standard notion of \(\varSigma \)structure \(\mathcal {M}\) and of truth of a formula in a \(\varSigma \)structure under a free variables assignment. The support of \(\mathcal {M}\) is denoted as \(\vert \mathcal {M}\vert \). The interpretation of a (function, predicate) symbol \(\sigma \) in \(\mathcal {M}\) is denoted \(\sigma ^{\mathcal {M}}\).
A \(\varSigma \)theory T is a set of \(\varSigma \)sentences; a model of T is a \(\varSigma \)structure \(\mathcal {M}\) where all sentences in T are true. We use the standard notation \(T\models \phi \) to say that \(\phi \) is true in all models of T for every assignment to the variables occurring free in \(\phi \). We say that \(\phi \) is Tsatisfiable iff there is a model \(\mathcal {M}\) of T and an assignment to the variables occurring free in \(\phi \) making \(\phi \) true in \(\mathcal {M}\).
We now focus on the constraint satisfiability problem and quantifier elimination for a theory T. A \(\varSigma \)formula \(\phi \) is a \(\varSigma \)constraint (or just a constraint) iff it is a conjunction of literals. The constraint satisfiability problem for T is the following: we are given a constraint \(\phi ({\underline{x}})\) and we are asked whether there exist a model \(\mathcal {M}\) of T and an assignment \(\mathcal {I}\) to the free variables \({\underline{x}}\) such that \(\mathcal {M}, \mathcal {I}\models \phi ({\underline{x}})\). A theory T has quantifier elimination iff for every formula \(\phi ({\underline{x}})\) in the signature of T there is a quantifierfree formula \(\phi '({\underline{x}})\) such that \(T\models \phi ({\underline{x}})\leftrightarrow \phi '({\underline{x}})\). Since we are in a computational logic context, when we speak of quantifier elimination, we assume that it is effective, namely that it comes with an algorithm for computing \(\phi '\) out of \(\phi \). It is wellknown that quantifier elimination holds in case we can eliminate quantifiers from primitive formulae, i.e., formulae of the kind \(\exists {\underline{y}}\,\phi ({\underline{x}}, {\underline{y}})\), with \(\phi \) a constraint.
We recall also some further basic notions. Let \(\varSigma \) be a firstorder signature. The signature obtained from \(\varSigma \) by adding to it a set \({\underline{a}}\) of new constants (i.e., 0ary function symbols) is denoted by \(\varSigma ^{{\underline{a}}}\). Analogously, given a \(\varSigma \)structure \(\mathcal {M}\), the signature \(\varSigma \) can be expanded to a new signature \(\varSigma ^{\mathcal {M}}:=\varSigma \cup \{\bar{a}\ \ a\in \mathcal {M} \}\) by adding a constant \(\bar{a}\) (the name for a) for each element a in the support of \(\mathcal {M}\), with the convention that two distinct elements are denoted by different “name” constants. \(\mathcal {M}\) can be expanded to a \(\varSigma ^{\mathcal {M}}\)structure \({\overline{\mathcal {M}}}:=(\mathcal {M}, a)_{a\in \vert \mathcal {M}\vert }\) just interpreting the additional constants over the corresponding elements. From now on, when the meaning is clear from the context, we will freely use the notation \(\mathcal {M}\) and \({\overline{\mathcal {M}}}\) interchangeably: in particular, given a \(\varSigma \)structure \(\mathcal {M}\) and a \(\varSigma \)formula \(\phi ({\underline{x}})\) with free variables that are all in \({\underline{x}}\), we will write, by abuse of notation, \(\mathcal {M}\models \phi ({\underline{a}})\) instead of \({\overline{\mathcal {M}}}\models \phi ({\bar{{\underline{a}}}})\).
We say that a theory T is stably infinite iff every Tsatisfiable constraint is satisfiable in an infinite model of T. Moreover, a theory T is convex iff for every constraint \(\delta \), if \(T\vdash \delta \rightarrow \bigvee _{i=1}^n x_i=y_i\) then \(T\vdash \delta \rightarrow x_i=y_i\) holds for some \(i\in \{1,\ldots , n\}\). Strictly speaking, convexity says that if, for a set of literals \(\phi \) and for a non empty disjunction of variables \(\bigvee _{i=1}^n x_i=y_i\), we have \(T\models \phi \rightarrow \bigvee _{i=1}^n x_i=y_i\), then we have also \(T\models \phi \rightarrow x_i=y_i\) for some \(i=1, \dots ,n\). If, instead of variables, we have terms, the same property nevertheless applies: if we have \(T\models \phi \rightarrow \bigvee _{i=1}^n t_i=u_i\), then for fresh variables \(x_i, y_i\) we get \(T\models \phi \wedge \bigwedge _{i=1}^n (x_i= t_i \wedge y_i=u_i)\rightarrow \bigvee _{i=1}^n x_i=y_i\), which implies, by applying the definition of convexity, the same property for terms.
A \(\varSigma \)homomorphism (or, simply, a homomorphism) between two \(\varSigma \)structures \(\mathcal {M}\) and \(\mathcal {N}\) is a map \(\mu : \vert \mathcal {M}\vert \longrightarrow \vert \mathcal {N}\vert \) among the support sets \(\vert \mathcal {M}\vert \) of \(\mathcal {M}\) and \(\vert \mathcal {N}\vert \) of \(\mathcal {N}\) satisfying the condition \((\mathcal {M}\models \varphi \quad \Rightarrow \quad \mathcal {N}\models \varphi )\) for all \(\varSigma ^{\vert \mathcal {M}\vert }\)atoms \(\varphi \) (\(\mathcal {M}\) is regarded as a \(\varSigma ^{\vert \mathcal {M}\vert }\)structure, by interpreting each additional constant \(a\in \vert \mathcal {M}\vert \) into itself and \(\mathcal {N}\) is regarded as a \(\varSigma ^{\vert \mathcal {M}\vert }\)structure by interpreting each additional constant \(a\in \vert \mathcal {M}\vert \) into \(\mu (a)\)). In case the last condition holds for all \(\varSigma ^{\mathcal {M}}\)literals, the homomorphism \(\mu \) is said to be an embedding and if it holds for all first order formulae, the embedding \(\mu \) is said to be elementary.
If \(\mu : \mathcal {M}\longrightarrow \mathcal {N}\) is an embedding which is just the identity inclusion \(\vert \mathcal {M}\vert \subseteq \vert \mathcal {N}\vert \), we say that \(\mathcal {M}\) is a substructure of \(\mathcal {N}\) or that \(\mathcal {N}\) is an extension of \(\mathcal {M}\). Universal theories can be characterized as those theories T having the property that if \(\mathcal {N}\models T\) and \(\mathcal {M}\) is a substructure of \(\mathcal {N}\), then \(\mathcal {M}\models T\) (see [11]). If \(\mathcal {M}\) is a structure and \(X\subseteq \vert \mathcal {M}\vert \), then there is the smallest substructure of \(\mathcal {M}\) including X in its support; this is called the substructure generated by X. If X is the set of elements of a finite tuple \({\underline{a}}\), then the substructure generated by X has in its support precisely the \(b\in \vert \mathcal {M}\vert \) such that \(\mathcal {M}\models b=t({\underline{a}})\) for some term t.
Let \(\mathcal {M}\) be a \(\varSigma \)structure. The diagram of \(\mathcal {M}\), written \(\varDelta _{\varSigma }(\mathcal {M})\) (or just \(\varDelta (\mathcal {M})\)), is the set of ground \(\varSigma ^{\mathcal {M}}\)literals that are true in \(\mathcal {M}\). An easy but important result, called Robinson Diagram Lemma [11], says that, given any \(\varSigma \)structure \(\mathcal {N}\), the embeddings \(\mu : \mathcal {M}\longrightarrow \mathcal {N}\) are in bijective correspondence with expansions of \(\mathcal {N}\) to \(\varSigma ^{\vert \mathcal {M}\vert }\)structures which are models of \(\varDelta _{\varSigma }(\mathcal {M})\). The expansions and the embeddings are related in the obvious way: \({\bar{a}}\) is interpreted as \(\mu (a)\).
3 Uniform Interpolants
We report the notion of a cover taken from [32] and also the basic results proved in [6, 10]. Fix a theory T and an existential formula \(\exists {\underline{e}}\, \phi ({\underline{e}}, {\underline{y}})\); call a residue of \(\exists {\underline{e}}\, \phi ({\underline{e}}, {\underline{y}})\) any quantifierfree formula belonging to the set of quantifierfree formulae(the above two sets are trivially equal, by applying the \(\exists \)left introduction rule). A quantifierfree formula \(\psi ({\underline{y}})\) is said to be a Tcover (or, simply, a cover) of \(\exists {\underline{e}}\, \phi ({\underline{e}},{\underline{y}})\) iff \(\psi ({\underline{y}})\in Res(\exists {\underline{e}}\, \phi )\) and \(\psi ({\underline{y}})\) implies (modulo T) all the other formulae in \(Res(\exists {\underline{e}}\, \phi )\). The following “coverbyextensions” Lemma [6] (to be widely used throughout the paper) supplies a semantic counterpart to the notion of a cover:
$$\begin{aligned} Res(\exists {\underline{e}}\, \phi )=\{\theta ({\underline{y}}, {\underline{z}})\mid T \models \phi ({\underline{e}}, {\underline{y}}) \rightarrow \theta ({\underline{y}}, {\underline{z}})\}=\{\theta ({\underline{y}}, {\underline{z}})\mid T \models \exists {\underline{e}}\,\phi ({\underline{e}}, {\underline{y}}) \rightarrow \theta ({\underline{y}}, {\underline{z}})\} \end{aligned}$$
Lemma 1
A formula \(\psi ({\underline{y}})\) is a Tcover of \(\exists {\underline{e}}\, \phi ({\underline{e}}, {\underline{y}})\) iff it satisfies the following two conditions:
(i)
\(T\models \forall {\underline{y}}\,( \exists {\underline{e}}\,\phi ({\underline{e}}, {\underline{y}}) \rightarrow \psi ({\underline{y}}))\);
(ii)
for every model \(\mathcal {M}\) of T, for every tuple of elements \({\underline{a}}\) from the support of \(\mathcal {M}\) such that \(\mathcal {M}\models \psi ({\underline{a}})\) it is possible to find another model \(\mathcal {N}\) of T such that \(\mathcal {M}\) embeds into \(\mathcal {N}\) and \(\mathcal {N}\models \exists {\underline{e}}\,\phi ({\underline{e}}, {\underline{a}})\).
Proof
See [6]. \(\square \)
We underline that, since our language is at most countable, we can assume that the models \(\mathcal {M}\), \(\mathcal {N}\) from (ii) above are at most countable too, by a LöwenheimSkolem argument.
We say that a theory T has uniform quantifierfree interpolation iff every existential formula \(\exists {\underline{e}}\, \phi ({\underline{e}},{\underline{y}})\) (equivalently, every primitive formula \(\exists {\underline{e}}\, \phi ({\underline{e}},{\underline{y}})\)) has a Tcover. Notice that a cover is also called (quantifierfree) uniform interpolant for the following reason. Indeed, it is clear that if T has uniform quantifierfree interpolation, then it has ordinary quantifierfree interpolation [2], in the sense that if we have \(T\models \phi ({\underline{e}}, {\underline{y}})\rightarrow \phi '({\underline{y}}, {\underline{z}})\) (for quantifierfree formulae \(\phi , \phi '\)), then there is a quantifierfree formula \(\theta ({\underline{y}})\) such that \(T\models \phi ({\underline{e}}, {\underline{y}})\rightarrow \theta ({\underline{y}})\) and \(T\models \theta ({\underline{y}})\rightarrow \phi '({\underline{y}}, {\underline{z}})\). In fact, if T has uniform quantifierfree interpolation, then the interpolant \(\theta \) is independent on \(\phi '\) (the same \(\theta ({\underline{y}})\) can be used as interpolant for all entailments \(T\models \phi ({\underline{e}}, {\underline{y}})\rightarrow \phi '({\underline{y}}, {\underline{z}})\), varying \(\phi '\)). Hence, it is straightforward to see that the definition of cover is equivalent to the one of uniform interpolant given in the introduction.
We say that a universal theory T has a model completion iff there is a stronger theory \(T^*\supseteq T\) (still within the same signature \(\varSigma \) of T) such that: Other equivalent definitions are possible [11]: for instance, (i) is equivalent to the fact that T and \(T^*\) prove the same universal formulae or again to the fact that every model of T can be embedded into a model of \(T^*\). We recall that the model completion, if it exists, is unique and that its existence implies the quantifierfree interpolation property for T [11] (the latter can be seen directly or via the correspondence between quantifierfree interpolation and amalgamability, see [2]).
(i)
every \(\varSigma \)constraint that is satisfiable in a model of T is satisfiable in a model of \(T^*\);
(ii)
\(T^*\) eliminates quantifiers.
A close relationship between model completion and uniform interpolation emerged in the area of propositional logic (see the book [25]) and can be formulated roughly as follows. It is wellknown that most propositional calculi, via Lindenbaum constructions, can be algebraized: the algebraic analogue of classical logic are Boolean algebras, the algebraic analogue of intuitionistic logic are Heyting algebras, the algebraic analogue of modal calculi are suitable varieties of modal algebras, etc. Under suitable hypotheses, it turns out that a propositional logic has uniform interpolation (for the global consequence relation) iff the equational theory axiomatizing the corresponding variety of algebras has a model completion [25]. In the context of first order theories, we prove an even more direct connection:
Theorem 1
Suppose that T is a universal theory. Then T has a model completion \(T^*\) iff T has uniform quantifierfree interpolation. If this happens, \(T^*\) is axiomatized by the infinitely many sentenceswhere \(\exists {\underline{e}}\, \phi ({\underline{e}}, {\underline{y}})\) is a primitive formula and \(\psi \) is a cover of it.
$$\begin{aligned} \forall {\underline{y}}\,(\psi ({\underline{y}}) \rightarrow \exists {\underline{e}}\, \phi ({\underline{e}}, {\underline{y}})), \end{aligned}$$
(1)
4 Equality Interpolating Condition and Beth Definability
We report here some definitions and results we need concerning combined quantifierfree interpolation. Most definitions and results come from [2], but are simplified here
because we restrict them to the case of universal convex theories.
We recall that a theory T is stably infinite iff every Tsatisfiable constraint is satisfiable in an infinite model of T. The following lemma comes from a compactness argument:
Lemma 2
If T is stably infinite, then every finite or countable model \(\mathcal {M}\) of T can be embedded in a model \(\mathcal {N}\) of T such that \(\vert \mathcal {N}\vert \setminus \vert \mathcal {M}\vert \) is countable.
Proof
Consider \(T\cup \varDelta (\mathcal {M})\cup \{c_i\ne a\, \mid \, a\in \vert \mathcal {M}\vert \}_i\cup \{c_i\ne c_j\}_{i\ne j}\), where \(\{c_i\}_i\) is a countable set of fresh constants: by the Diagram Lemma and the downward LöwenheimSkolem theorem [11], it is sufficient to show that this set is consistent
(in fact if this set is consistent, there will be a superstructure \(\mathcal {N}\) of \(\mathcal {M}\) in which the countably many constants \(c_i\) will be interpreted on elements which are different from each others and also different from the elements from the support of \(\mathcal {M}\)).
Suppose the above set is not consistent; then by compactness \(T\cup \varDelta _0\cup \varDelta _1\cup \varDelta _2\) is not satisfiable, for a finite subset \(\varDelta _0\) of \(\varDelta (\mathcal {M})\), a finite subset \(\varDelta _1\) of \( \{c_i\ne a\, \mid \, a\in \vert \mathcal {M}\vert \}_i\) and a finite subset \(\varDelta _2\) of \(\cup \{c_i\ne c_j\}_{i\ne j}\). However, this is a contradiction because by stable infiniteness \(\varDelta _0\) (being satisfiable in \(\mathcal {M}\)) is satisfiable in an infinite model of T. \(\square \)
We also recall that theory T is convex iff for every constraint \(\delta \), if \(T\vdash \delta \rightarrow \bigvee _{i=1}^n x_i=y_i\) then \(T\vdash \delta \rightarrow x_i=y_i\) holds for some \(i\in \{1,\ldots , n\}\).
A convex theory T is ‘almost’ stably infinite in the sense that it can be shown that every constraint which is Tsatisfiable in a Tmodel whose support has at least two elements is satisfiable also in an infinite Tmodel. The oneelement model can be used to build counterexamples, though: e.g., the theory of Boolean algebras is convex (like any other universal Horn theory) but the constraint \(x=0 \wedge x=1\) is only satisfiable in the degenerate oneelement Boolean algebra. Since we take into account these limit cases, we do not assume that convexity implies stable infiniteness.
Definition 1
A convex universal theory T is equality interpolating iff
for every pair \(y_1, y_2\) of variables and for every pair of constraints \(\delta _1({\underline{x}},{\underline{z}}_1, y_1), \delta _2({\underline{x}},{\underline{z}}_2,y_2)\) such thatthere exists a term \(t({\underline{x}})\) such that
$$\begin{aligned} T\vdash \delta _1({\underline{x}}, {\underline{z}}_1,y_1)\wedge \delta _2({\underline{x}},{\underline{z}}_2, y_2)\rightarrow y_1= y_2 \end{aligned}$$
(2)
$$\begin{aligned} T\vdash \delta _1({\underline{x}}, {\underline{z}}_1, y_1)\wedge \delta _2({\underline{x}}, {\underline{z}}_2, y_2)\rightarrow y_1= t({\underline{x}}) \wedge y_2= t({\underline{x}}). \end{aligned}$$
(3)
Quantifierfree interpolation and combined quantifierfree interpolation can be semantically characterized, as we are going to show.
Definition 2
A universal theory T has the amalgamation property iff whenever we are given models \(\mathcal {M}_1\) and \(\mathcal {M}_2\) of T and
their common substructure \(\mathcal {M}_0\), there exists a further model \(\mathcal {M}\) of T endowed with embeddings \(\mu _1:\mathcal {M}_1 \longrightarrow \mathcal {M}\) and \(\mu _2:\mathcal {M}_2 \longrightarrow \mathcal {M}\) whose restrictions to \(\mathcal {M}_0\) coincide.
A universal theory T has the strong amalgamation property if the above embeddings \(\mu _1, \mu _2\) and the above model \(\mathcal {M}\) can be chosen so as to satisfy the following additional condition: if for some \(m_1, m_2\) we have \(\mu _1(m_1)=\mu _2(m_2)\), then there exists an element a in \(\mathcal {M}_0\) such that \(m_1=a=m_2\).
Theorem 2
[2] The following two conditions are equivalent for a convex universal theory T:
(i)
T is equality interpolating and has quantifierfree interpolation;
(ii)
T has the strong amalgamation property.
Proof
For the sake of completeness, we report the proof of the implication (i) \(\Rightarrow \) (ii) (this is the only fact used in the paper). Suppose that T is equality interpolating and has quantifierfree interpolation; we prove that it is strongly amalgamable. If the latter property fails, by Robinson Diagram Lemma, there exist models \(\mathcal {M}_1, \mathcal {M}_2\) of T together with a shared submodel \(\mathcal {A}\) such that the set of sentencesis not Tconsistent. By compactness, the sentenceis Tvalid, for some tuples \({\underline{a}}\subseteq \vert \mathcal {A}\vert \), \({\underline{m}}_1\subseteq (\vert \mathcal {M}_1\vert \setminus \vert \mathcal {A}\vert )\), \({\underline{m}}_2\subseteq (\vert \mathcal {M}_2\vert \setminus \vert \mathcal {A}\vert )\) and for some ground formulae \(\delta _1({\underline{a}}, {\underline{m}}_1),\delta _{2}({\underline{a}}, {\underline{m}}_2)\) true in \(\mathcal {M}_1, \mathcal {M}_2\), respectively.
$$\begin{aligned} \varDelta _{\varSigma }(\mathcal {M}_1)\cup \varDelta _{\varSigma }(\mathcal {M}_2)\cup \{ m_1\ne m_2~\vert ~ m_1\in \vert \mathcal {M}_1\vert \setminus \vert \mathcal {A}\vert , ~ m_2\in \vert \mathcal {M}_2\vert \setminus \vert \mathcal {A}\vert \} \end{aligned}$$
$$\begin{aligned} \delta _1({\underline{a}}, {\underline{m}}_1)\wedge \delta _{2}({\underline{a}}, {\underline{m}}_2) \rightarrow \bigvee _{n_1\in {\underline{m}}_1, n_2\in {\underline{m}}_2} n_1= n_2 \end{aligned}$$
If the disjunction is empty, we get \(T\models \delta _1({\underline{a}}, {\underline{m}}_1) \rightarrow \lnot \delta _{2}({\underline{a}}, {\underline{m}}_2)\) and then we get a contradiction by the quantifierfree interpolation property (the argument is the same as below). Otherwise, by convexity, there are \(n_1\in {\underline{m}}_1, n_2\in {\underline{m}}_2\) such thatis Tvalid. By the equality interpolating property, there is a term \(t({\underline{a}})\) such thatis Tvalid. By the quantifierfree interpolation property, there is a quantifierfree formula \(\theta ({\underline{a}})\) such thatandare both Tvalid. Since \(n_1\in \vert \mathcal {M}_1\vert \setminus \vert \mathcal {A}\vert \), we have that \(n_1\ne t({\underline{a}})\) is true in \(\mathcal {M}_1\). But then we have a contradiction because \(\theta ({\underline{a}})\) is true in \(\mathcal {M}_1\), \(\mathcal {A}\) and in \(\mathcal {M}_2\) as well (truth of quantifierfree formulae moves back and forth via substructures). \(\square \)
$$\begin{aligned} \delta _1({\underline{a}}, {\underline{m}}_1)\wedge \delta _{2}({\underline{a}}, {\underline{m}}_2) \rightarrow n_1=n_2 \end{aligned}$$
$$\begin{aligned} \delta _1({\underline{a}}, {\underline{m}}_1)\wedge \delta _{2}({\underline{a}}, {\underline{m}}_2) \rightarrow n_1=t({\underline{a}}) \end{aligned}$$
$$\begin{aligned} \delta _1({\underline{a}}, {\underline{m}}_1)\wedge n_1\ne t({\underline{a}}) \rightarrow \theta ({\underline{a}}) \end{aligned}$$
$$\begin{aligned} \theta ({\underline{a}}) \rightarrow \lnot \delta _{2}({\underline{a}}, {\underline{m}}_2) \end{aligned}$$
We underline that Theorem 2 extends also to the non convex case provided the notion of an equality interpolating theory is suitably adjusted [2].
Next two results (supplied without proof) will be used only in Sect. 6.1 to show that, in some sense, the sufficient conditions of our main combination Theorem 5 are also necessary.
Theorem 3
The previous theorem essentially states that the equality interpolating property is a sufficient condition for the transfer of quantifierfree interpolation to theory combinations. There is a converse of the previous result, in the sense that it is possible to show that the equality interpolating property is, to some extent, necessary in order to guarantee the transfer of quantifierfree interpolation for minimal combinations with signatures adding only uninterpreted symbols. For this purpose, for a signature \(\varSigma \), we call \(\mathcal {EUF}(\varSigma )\) the pure equality theory over the signature \(\varSigma \) (this theory is equality interpolating and has the quantifierfree interpolation property).
Theorem 4
[2] Let T be a stably infinite, universal, convex theory admitting quantifierfree interpolation and let \(\varSigma \) be a signature disjoint from the signature of T containing at least a unary predicate symbol. Then, \(T\cup \mathcal {EUF}(\varSigma )\) has quantifierfree interpolation iff T is equality interpolating.
In [2] the above definitions and results are extended to the nonconvex case and a long list of universal quantifierfree interpolating and equality interpolating theories is given. The list includes \(\mathcal {EUF}(\varSigma )\), recursive data theories, as well as linear arithmetics. For linear arithmetics (and fragments of its), it is essential to make a very careful choice of the signature, see again [2] (especially Subsection 4.1) for details. All the above theories admit a model completion (which coincides with the theory itself in case the theory admits quantifier elimination).
The equality interpolating property in a theory T can be equivalently characterized using Beth definability as follows. Consider a primitive formula \(\exists {\underline{z}}\phi ({\underline{x}}, {\underline{z}},y)\) (here \(\phi \) is a conjunction of literals); we say that \(\exists {\underline{z}}\, \phi ({\underline{x}}, {\underline{z}},y)\) implicitly defines y in T iff the formulais Tvalid. We say that \(\exists {\underline{z}}\phi ({\underline{x}}, {\underline{z}},y)\) explicitly defines y in T iff there is a term \(t({\underline{x}})\) such that the formulais Tvalid.
$$\begin{aligned} \forall y \,\forall y'\;( \exists {\underline{z}}\phi ({\underline{x}}, {\underline{z}},y)\wedge \exists {\underline{z}}\phi ({\underline{x}}, {\underline{z}},y') \rightarrow y= y') \end{aligned}$$
(4)
$$\begin{aligned} \forall y \;( \exists {\underline{z}}\phi ({\underline{x}}, {\underline{z}},y) \rightarrow y= t({\underline{x}})) \end{aligned}$$
(5)
For future use, we notice that, by trivial logical manipulations, the formulae (4) and (5) are logically equivalent toand torespectively (we shall use such equivalences without explicit mention).
$$\begin{aligned} \forall y\forall {\underline{z}}\forall y'\forall {\underline{z}}'( \phi ({\underline{x}}, {\underline{z}},y)\wedge \phi ({\underline{x}}, {\underline{z}}',y') \rightarrow y= y')~~~. \end{aligned}$$
(6)
$$\begin{aligned} \forall y \forall {\underline{z}}(\phi ({\underline{x}}, {\underline{z}},y) \rightarrow y= t({\underline{x}})) \end{aligned}$$
(7)
We say that a theory T has the Beth definability property for primitive formulae iff whenever a primitive formula \(\exists {\underline{z}}\, \phi ({\underline{x}}, {\underline{z}},y)\) implicitly defines the variable y then it also explicitly defines it.
Proposition 1
[2] A convex equality interpolating theory T
has the Beth definability property for primitive formulae.
Proof
Suppose that T is equality interpolating and thatthen there is a term \(t({\underline{x}})\) such thatReplacing \({\underline{z}}',y'\) by \({\underline{z}},y\) via a substitution, we get precisely (7). \(\square \)
$$\begin{aligned} T\vdash \phi ({\underline{x}}, {\underline{z}},y)\wedge \phi ({\underline{x}}, {\underline{z}}',y') \rightarrow y= y'~~; \end{aligned}$$
$$\begin{aligned} T\vdash \phi ({\underline{x}}, {\underline{z}},y)\wedge \phi ({\underline{x}}, {\underline{z}}',y') \rightarrow y=t({\underline{x}}) \wedge y'=t({\underline{x}})~~. \end{aligned}$$
We remark that the above Proposition can be inverted (see [2]).
5 Convex Theories
We now collect some useful facts concerning convex theories. We fix for this section a convex, stably infinite, equality interpolating universal theory T admitting a model completion \(T^*\). We let \(\varSigma \) be the signature of T. We fix also a \(\varSigma \)constraint \(\phi ({\underline{x}}, {\underline{y}})\), where we assume that \({\underline{y}}=y_1, \dots , y_n\) (recall that the tuple \({\underline{x}}\) is disjoint from the tuple \({\underline{y}}\) according to our conventions from Sect. 2).
For \(i=1, \dots , n\), we let the formula \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}})\) be the quantifierfree formula equivalent in \(T^*\) to the formulawhere the \({\underline{y}}'\) are renamed copies of the \({\underline{y}}\). Notice that the variables occurring free in \(\phi \) are \({\underline{x}}, {\underline{y}}\), whereas only the \({\underline{x}}\) occur free in \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}})\) (the variable \(y_i\) is among the \({\underline{y}}\) and does not occur free in \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}})\)): these facts coming from our notational conventions are crucial and should be kept in mind when reading this and next section. We need a first semantic technical lemma.
$$\begin{aligned} \forall {\underline{y}}\, \forall {\underline{y}}' (\phi ({\underline{x}}, {\underline{y}}) \wedge \phi ({\underline{x}}, {\underline{y}}')\rightarrow y_i= y'_i) \end{aligned}$$
(8)
Lemma 3
Suppose that we are given a model \(\mathcal {M}\) of T and elements \({\underline{a}}\) from the support of \(\mathcal {M}\) such that \(\mathcal {M}\not \models \mathtt {ImplDef}_{\phi ,y_i}^T({\underline{a}})\) for all \(i=1, \dots ,n\). Then there exists an extension \(\mathcal {N}\) of \(\mathcal {M}\) such that
for some \({\underline{b}}\in \vert \mathcal {N}\vert \setminus \vert \mathcal {M}\vert \) we have \(\mathcal {N}\models \phi ({\underline{a}}, {\underline{b}})\).
Proof
Since T has a model completion, it has uniform quantifierfree interpolants by Theorem 1, hence it has also (ordinary) quantifierfree interpolants. By Theorem 2 it is strongly amalgamable because it is equality interpolating. In conclusion, we are allowed to use strong amalgamation in our proof. By strong amalgamability, we can freely assume that \(\mathcal {M}\) is generated, as a \(\varSigma \)structure, by the \({\underline{a}}\): in fact, if we prove the statement for the substructure generated by the \({\underline{a}}\), then strong amalgamability will provide the model we want.
By using the Robinson Diagram Lemma, what we need is to prove the consistency of \(T\cup \varDelta (\mathcal {M})\) with the set of ground sentenceswhere \(t({\underline{x}})\) varies over \(\varSigma ({\underline{x}})\)terms, the \({\underline{b}}=b_1, \dots , b_n\) are fresh constants and i vary over \(1, \dots , n\). By convexity,^{1} this set is inconsistent iff there exist a term \(t({\underline{x}})\) and \(i=1, \dots , n\) such thatThis however implies that \(T\cup \varDelta (\mathcal {M})\) has the formulaas a logical consequence. If we now embed \(\mathcal {M}\) into a model \(\mathcal {N}\) of \(T^*\), we have that \(\mathcal {N}\models \mathtt {ImplDef}_{\phi ,y_i}^T({\underline{a}})\), which is in contrast to \(\mathcal {M}\not \models \mathtt {ImplDef}_{\phi ,y_i}^T({\underline{a}})\) (because \(\mathcal {M}\) is a substructure of \(\mathcal {N}\) and \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{a}})\) is quantifierfree). \(\square \)
$$\begin{aligned} \{\phi ({\underline{a}}, {\underline{b}})\} \cup \{ b_i\ne t({\underline{a}})\}_{t,b_i} \end{aligned}$$
$$\begin{aligned} T\cup \varDelta (\mathcal {M})\vdash \phi ({\underline{a}}, {\underline{y}})\rightarrow y_i=t({\underline{a}}). \end{aligned}$$
$$\begin{aligned} \forall {\underline{y}}\, \forall {\underline{y}}' (\phi ({\underline{a}}, {\underline{y}}) \wedge \phi ({\underline{a}}, {\underline{y}}')\rightarrow y_i= y'_i) \end{aligned}$$
The following lemma supplies terms which will be used as ingredients in our combined covers algorithm:
Lemma 4
Let \(L_{i1}({\underline{x}})\vee \cdots \vee L_{ik_i}({\underline{x}})\) be the disjunctive normal form (DNF) of \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}})\). Then, for every \(j=1, \dots , k_i\), there is a \(\varSigma ({\underline{x}})\)term \(t_{ij}({\underline{x}})\) such thatAs a consequence, a formula of the kind \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}}) \wedge \exists {\underline{y}}\, (\phi ({\underline{x}}, {\underline{y}})\wedge \psi )\) is equivalent (modulo T) to the formula
$$\begin{aligned} T\vdash L_{ij}({\underline{x}})\wedge \phi ({\underline{x}},{\underline{y}})\rightarrow y_i=t_{ij}. \end{aligned}$$
(9)
$$\begin{aligned} \bigvee _{j=1}^{k_i} \exists {\underline{y}}\; (y_i=t_{ij} \wedge L_{ij}({\underline{x}}) \wedge \phi ({\underline{x}}, {\underline{y}})\wedge \psi ). \end{aligned}$$
(10)
Proof
We have that \((\bigvee _j L_{ij})\leftrightarrow \mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}})\) is a tautology, hence from the definition of \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}})\), we have thathowever this formula is trivially equivalent to a universal formula (\(L_{ij}\) does not depend on \({\underline{y}},{\underline{y}}'\)), hence since T and \(T^*\) prove the same universal formulae, we getUsing Beth definability property (Proposition 1), we get (9), as required, for some terms \(t_{ij}({\underline{x}})\). Finally, the second claim of the lemma follows from (9) by trivial logical manipulations. \(\square \)
$$\begin{aligned} T^*\vdash L_{ij}({\underline{x}})\rightarrow \forall {\underline{y}}\, \forall {\underline{y}}' (\phi ({\underline{x}}, {\underline{y}}) \wedge \phi ({\underline{x}}, {\underline{y}}')\rightarrow y_i= y'_i); \end{aligned}$$
$$\begin{aligned} T\vdash L_{ij}({\underline{x}}) \wedge \phi ({\underline{x}}, {\underline{y}}) \wedge \phi ({\underline{x}}, {\underline{y}}')\rightarrow y_i= y'_i. \end{aligned}$$
In all our concrete examples, the theory T has a decidable quantifierfree fragment (namely it is decidable whether a quantifierfree formula is a logical consequence of T or not), thus the terms \(t_{ij}\) mentioned in Lemma 4 can be computed just by enumerating all possible \(\varSigma ({\underline{x}})\)terms: the computation terminates, because the above proof shows that the appropriate terms always exist. However, this is terribly inefficient and, from a practical point of view, one needs to have at disposal dedicated algorithms to find the required equality interpolating terms. For some common theories (\(\mathcal {EUF}\), Lispstructures, linear real arithmetic), such algorithms are designed in [47]; in [2] [Lemma 4.3 and Theorem 4.4], the algorithms for computing equality interpolating terms are connected to quantifier elimination algorithms in the case of universal theories admitting quantifier elimination.
The following lemma will be useful in the next section:
Lemma 5
Let T have a model completion \(T^*\) and let the constraint \(\phi ({\underline{x}},{\underline{y}})\) be of the kind \(\alpha ({\underline{x}})\wedge \phi '({\underline{x}},{\underline{y}})\), where \({\underline{y}}=y_1,\dots , y_n\). Then for every \(i=1, \dots , n\), the formula \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}})\) is Tequivalent to \(\alpha ({\underline{x}})\rightarrow \mathtt {ImplDef}_{\phi ',y_i}^T({\underline{x}})\).
Proof
According to (8), the formula \(\mathtt {ImplDef}_{\phi ,y_i}^T({\underline{x}})\) is obtained by eliminating quantifiers in \(T^*\) fromThe latter is equivalent, modulo logical manipulations, towhence the claim (eliminating quantifiers in \(T^*\) from (11) and (12) gives quantifiersfree \(T^*\)equivalent formulae, hence also Tequivalent formulae because T and \(T^*\) prove the same quantifierfree formulae). \(\square \)
$$\begin{aligned} \forall {\underline{y}}\, \forall {\underline{y}}' (\alpha ({\underline{x}})\wedge \phi '({\underline{x}}, {\underline{y}}) \wedge \alpha ({\underline{x}})\wedge \phi '({\underline{x}}, {\underline{y}}')\rightarrow y_i= y'_i) \end{aligned}$$
(11)
$$\begin{aligned} \alpha ({\underline{x}})\rightarrow \forall {\underline{y}}\, \forall {\underline{y}}' (\phi '({\underline{x}}, {\underline{y}}) \wedge \phi '({\underline{x}}, {\underline{y}}')\rightarrow y_i= y'_i) \end{aligned}$$
(12)
6 The Convex Combined Cover Algorithm
Let us now fix two theories \(T_1, T_2\) over disjoint signatures \(\varSigma _1, \varSigma _2\).
We assume that both of them satisfy the assumptions from the previous section, meaning that they are convex, stably infinite, equality interpolating, universal and admit model completions \(T^*_1, T^*_2\) respectively. We will prove in this section (Theorem 5) that \(T_1\cup T_2\) admits a model completion too. We achieve this by supplying a combined algorithm, called \(\mathsf {ConvexCombCover}\), for computing \(T_1\cup T_2\)covers: in order to construct the \(T_1\cup T_2\)cover, this combined algorithm exploits the cover algorithms of the component theories \(T_i\) (\(i=1,2\)).
We need to compute a cover for \(\exists {\underline{e}}\,\phi ({\underline{x}}, {\underline{e}})\), where \(\phi \) is a conjunction of \(\varSigma _1\cup \varSigma _2\)literals. By applying rewriting purification steps like(where d is a fresh variable and t is a pure term, i.e. it is either a \(\varSigma _1\) or a \(\varSigma _2\)term), we can assume that our formula \(\phi \) is of the kind \(\phi _1\wedge \phi _2\), where \(\phi _1\) is a \(\varSigma _1\)formula and \(\phi _2\) is a \(\varSigma _2\)formula. Thus we need to compute a cover for a formula of the kindwhere \(\phi _i\) is a conjunction of \(\varSigma _i\)literals (\(i=1,2\)). By guessing a partition of the \({\underline{e}}\) and by replacing each variable e in \({\underline{e}}\) with the representative element of its equivalence class, we also assume that both \(\phi _1\) and \(\phi _2\) contain the literals \(e_i\ne e_j\) (for \(i\ne j\)) as a conjunct.
$$\begin{aligned} \phi \Longrightarrow \exists d\, (d=t \wedge \phi (d/t)) \end{aligned}$$
$$\begin{aligned} \exists {\underline{e}}\,(\phi _1({\underline{x}}, {\underline{e}})\wedge \phi _2({\underline{x}}, {\underline{e}})), \end{aligned}$$
(13)
Remark 1
It is not clear whether this preliminary guessing step can be avoided. In fact, NelsonOppen [38] combined satisfiability for convex theories does not need it; however, combining covers algorithms is a more complicated problem than combining mere satisfiability algorithms and for technical reasons related to the correctness and completeness proofs below, we were forced to introduce guessing at this step.
To manipulate formulae, our algorithm employs acyclic explicit definitions as follows. When we write \(\mathtt {ExplDef}({\underline{z}}, {\underline{x}})\) (where \({\underline{z}}, {\underline{x}}\) are tuples of distinct variables), we mean any formula of the kind (let \({\underline{z}}:=z_1 \dots , z_m\))where the term \(t_i\) is pure (i.e. it is a \(\varSigma _i\)term) and only the variables \(z_1, \dots , z_{i1}, {\underline{x}}\) can occur in it. We notice that an existential formula like \(\exists {\underline{z}}\;(\mathtt {ExplDef}({\underline{z}}, {\underline{x}})\wedge \psi ({\underline{z}}, {\underline{x}}))\) can be equivalently converted into a quantifierfree formula: indeed, since the ’explicit definitions’ \(z_i =t_i\) are in fact arranged acyclically, the existentially quantified variables \({\underline{z}}\) can be recursively eliminated by substituting them with terms containing eventually only the parameters \({\underline{x}}\).
$$\begin{aligned} \bigwedge _{i=1}^m z_i =t_i(z_1,\dots ,z_{i1},{\underline{x}}) \end{aligned}$$
A working formula is a formula of the kindwhere \(\psi _1\) is a conjunction of \(\varSigma _1\)literals and \(\psi _2\) is a conjunction of \(\varSigma _2\)literals. The variables \({\underline{x}}\) are called parameters, the variables \({\underline{z}}\) are called defined variables and the variables \({\underline{e}}\) (truly) existential variables. The parameters do not change during the execution of the algorithm. We assume that \(\psi _1, \psi _2\) in a working formula (14) always contain the literals \(e_i\ne e_j\) (for distinct \(e_i, e_j\) from \({\underline{e}}\)) as a conjunct.
$$\begin{aligned} \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}})))~~, \end{aligned}$$
(14)
In our starting formula (13), there are no defined variables. However, if via some syntactic check it happens that some of the existential variables can be recognized as defined, then it is useful to display them as such (this observation may avoid redundant cases  leading to inconsistent disjuncts  in the computations below).
A working formula like (14) is said to be terminal iff for every existential variable \(e_i\in {\underline{e}}\) we have thatRoughly speaking, we can say that in a terminal working formula, all variables which are not parameters are either explicitly definable or recognized as not implicitly definable by both theories; of course, a working formula with no existential variables is terminal.
$$\begin{aligned} T_1\vdash \psi _1\rightarrow \lnot \mathtt {ImplDef}_{\psi _1,e_i}^{T_1}({\underline{x}},{\underline{z}}) ~~\mathrm{and}~~T_2\vdash \psi _2\rightarrow \lnot \mathtt {ImplDef}_{\psi _2,e_i}^{T_2}({\underline{x}},{\underline{z}})~~~. \end{aligned}$$
(15)
Lemma 6
Every working formula is equivalent (modulo \(T_1\cup T_2\)) to a disjunction of terminal working formulae.
Proof
To compute the required terminal working formulae, it is sufficient to apply the following nondeterministic procedure (the output is the disjunction of all possible outcomes). The nondeterministic procedure applies one of the following alternatives.
(1)
Update \(\psi _1\) by adding to it a disjunct from the DNF of \(\bigwedge _{e_i\in {\underline{e}}} \lnot \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}}} \lnot \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 4)^{2} is added to \(\mathtt {ExplDef}({\underline{z}}, {\underline{x}})\); the variable \(e_i\) becomes in this way part of the defined variables.
Notice that in alternative (2.i), the index i in the label (2.i) refers to the variable \(e_i\) chosen from \({\underline{e}}\).
If alternative (1) is chosen, the procedure stops, otherwise it is recursively applied again and again: we have one truly existential variable less after applying alternative (2.i), so the procedure terminates, since eventually either no truly existential variable remains or alternative (1) is applied. The correctness of the procedure is due to the fact that the following formula is trivially a tautology:The first disjunct is used in alternative (1), the other disjuncts in alternative (2.i). At the end of the procedure, we get a terminal working formula. Indeed, if no truly existential variable remains, then the working formula is trivially terminal. It remains to prove that the working formula obtained after applying alternative (1) is indeed terminal. Let \(\psi '_k\) (for \(k=1,2\)) be the formula obtained from \(\psi _k\) after applying alternative (1). We have that \(\psi '_k\) is \(\alpha ({\underline{x}},{\underline{z}})\wedge \psi _k({\underline{x}},{\underline{z}},{\underline{e}})\), where \(\alpha \) is a disjunct of the DNF of \(\bigwedge _{e_i\in {\underline{e}}} \lnot \mathtt {ImplDef}_{\psi _k,e_i}^{T_k}({\underline{x}},{\underline{z}})\). We need to show that \(T_k\vdash \psi '_k\rightarrow \lnot \mathtt {ImplDef}_{\psi '_k,e_j}^{T_k}({\underline{x}},{\underline{z}})\) for every j. Fix such a j; according to Lemma 5, we must show thatwhich is indeed the case because \(\alpha ({\underline{x}},{\underline{z}})\) logically implies \(\lnot \mathtt {ImplDef}_{\psi '_k,e_j}^{T_k}({\underline{x}},{\underline{z}})\), since \(\alpha ({{\underline{x}}}, {{\underline{z}}})\) is a disjunct of the DNF of \(\bigwedge _{e_i\in {\underline{e}}} \lnot \mathtt {ImplDef}_{\psi _k,e_i}^{T_k}({\underline{x}},{\underline{z}})\). \(\square \)
$$\begin{aligned}&\left( \bigwedge _{e_i\in {\underline{e}}} \lnot \mathtt {ImplDef}_{\psi _1,e_i}^{T_1}({\underline{x}},{\underline{z}})\wedge \bigwedge _{e_i\in {\underline{e}}} \lnot \mathtt {ImplDef}_{\psi _2,e_i}^{T_2}({\underline{x}},{\underline{z}}) \right) \vee \\&\vee ~\bigvee _{e_i\in {\underline{e}}} \mathtt {ImplDef}_{\psi _1,e_i}^{T_1}({\underline{x}},{\underline{z}}) \vee \bigvee _{e_i\in {\underline{e}}} \mathtt {ImplDef}_{\psi _2,e_i}^{T_2}({\underline{x}},{\underline{z}})~~~~~~ \end{aligned}$$
$$\begin{aligned} T_k\vdash \alpha ({\underline{x}}, {\underline{z}})\wedge \psi _k({\underline{x}},{\underline{z}}, {\underline{e}})\rightarrow \lnot (\alpha ({\underline{x}}, {\underline{z}})\rightarrow \mathtt {ImplDef}_{\psi _k,e_j}^{T_k}({\underline{x}},{\underline{z}})) \end{aligned}$$
Thus we are left to the problem of computing a cover of a terminal working formula; this problem is solved in the following proposition:
Proposition 2
A cover of a terminal working formula (14) can be obtained just by unravelling the explicit definitions of the variables \({\underline{z}}\) from the formulawhere \(\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}})\).
$$\begin{aligned} \exists {\underline{z}}\; (\mathtt {ExplDef}({\underline{z}}, {\underline{x}}) \wedge \theta _1({\underline{x}}, {\underline{z}}) \wedge \theta _2({\underline{x}},{\underline{z}})) \end{aligned}$$
(16)
Proof
In order to show that Formula (16) is the \(T_1\cup T_2\)cover of a terminal working formula (14), we apply Lemma 1. The first condition of that lemma is easily fulfilled. Concerning the second condition, we prove
that, for every \(T_1\cup T_2\)model \(\mathcal {M}\), for every tuple \({\underline{a}}, {\underline{c}}\) from \(\vert \mathcal {M}\vert \) such that \(\mathcal {M}\models \theta _1({\underline{a}}, {\underline{c}}) \wedge \theta _2({\underline{a}},{\underline{c}})\) there is an extension \(\mathcal {N}\) of \(\mathcal {M}\) such that \(\mathcal {N}\) is still a model of \(T_1\cup T_2\) and \(\mathcal {N}\models \exists {\underline{e}}(\psi _1({\underline{a}}, {\underline{c}}, {\underline{e}}) \wedge \psi _2({\underline{a}},{\underline{c}}, {\underline{e}}))\).
By a Löwenheim–Skolem argument, since our languages are countable, we can suppose that \(\mathcal {M}\) is at most countable and actually that it is countable by stable infiniteness of our theories, see Lemma 2 (the fact that \(T_1\cup T_2\) is stably infinite in case both \(T_1, T_2\) are such, comes from the proof of NelsonOppen combination result, see [17, 38, 44]).
According to the conditions (15) and the definition of a cover (notice that the formulae \(\lnot \mathtt {ImplDef}_{\psi _h,e_i}^{T_h}({\underline{x}},{\underline{z}})\) do not contain the \({\underline{e}}\) and are quantifierfree) we have that(for every \(e_i\in {\underline{e}}\)). Thus, since \(\mathcal {M}\not \models \mathtt {ImplDef}_{\psi _1,e_i}^{T_1}({\underline{a}},{\underline{c}})\) and \(\mathcal {M}\not \models \mathtt {ImplDef}_{\psi _2,e_i}^{T_2}({\underline{a}},{\underline{c}})\) hold for every \(e_i\in {\underline{e}}\), we can apply Lemma 3 and conclude that there exist a \(T_1\)model \(\mathcal {N}_1\) and a \(T_2\)model \(\mathcal {N}_2\) such that \(\mathcal {N}_1\models \psi _1({\underline{a}}, {\underline{c}}, {\underline{b}}_1)\) and \(\mathcal {N}_2\models \psi _2({\underline{a}}, {\underline{c}}, {\underline{b}}_2)\) for tuples \({\underline{b}}_1\in \vert \mathcal {N}_1\vert \) and \({\underline{b}}_2\in \vert \mathcal {N}_2\vert \), both disjoint from \(\vert \mathcal {M}\vert \). By a LöwenheimSkolem argument, we can suppose that \(\mathcal {N}_1, \mathcal {N}_2\) are countable and by Lemma 2 even that they are both countable extensions of \(\mathcal {M}\).
$$\begin{aligned} T_1\vdash \theta _1\rightarrow \lnot \mathtt {ImplDef}_{\psi _1,e_i}^{T_1}({\underline{x}},{\underline{z}}) ~~\mathrm{and}~~T_2\vdash \theta _2\rightarrow \lnot \mathtt {ImplDef}_{\psi _2,e_i}^{T_2}({\underline{x}},{\underline{z}}) \end{aligned}$$
The tuples \({\underline{b}}_1\) and \({\underline{b}}_2\) have equal length because the \(\psi _1, \psi _2\) from our working formulae entail \(e_i \ne e_j\), where \(e_i, e_j\) are different existential variables. Thus there is a bijection \(\iota : \vert \mathcal {N}_1\vert \rightarrow \vert \mathcal {N}_2\vert \) fixing all elements in \(\mathcal {M}\) and mapping componentwise the \({\underline{b}}_1\) onto the \({\underline{b}}_2\). But this means that, exactly as it happens in the proof of the completeness of the NelsonOppen combination procedure, the \(\varSigma _2\)structure on \(\mathcal {N}_2\) can be moved back via \(\iota ^{1}\) to \(\vert \mathcal {N}_1\vert \) in such a way that the \(\varSigma _2\)substructure from \(\mathcal {M}\) is fixed and in such a way that the tuple \({\underline{b}}_2\) is mapped to the tuple \({\underline{b}}_1\). In this way, \(\mathcal {N}_1\) becomes a \(\varSigma _1\cup \varSigma _2\)structure which is a model of \(T_1\cup T_2\) and which is such that \(\mathcal {N}_1\models \psi _1({\underline{a}}, {\underline{c}}, {\underline{b}}_1) \wedge \psi _2({\underline{a}},{\underline{c}}, {\underline{b}}_1)\), as required. \(\square \)
Theorem 5
Let \(T_1, T_2\) be convex, stably infinite, equality interpolating, universal theories over disjoint signatures admitting a model completion. Then \(T_1\cup T_2\) admits a model completion too. Covers in \(T_1\cup T_2\) can be effectively computed as shown above.
We recall from Theorem 3 that the equality interpolating property transfers to combination of theories too, when it holds in the component theories.
We now summarize the steps of the combined cover algorithm \(\mathsf {ConvexCombCover}\) that takes as input the primitive formula \(\exists {\underline{e}}\,\phi ({\underline{x}}, {\underline{e}})\), where \(\phi \) is a conjunction of \(\varSigma _1\cup \varSigma _2\)literals: Notice that the input cover algorithms in the above combined cover computation algorithm are used not only in the final step described in Proposition 2, but also every time we need to compute a formula \(\mathtt {ImplDef}_{\psi _h,e_i}^{T_h}({\underline{x}},{\underline{z}})\): according to its definition, this formula is obtained by eliminating quantifiers in \(T_i^*\) from (8) (this is done via a cover computation, reading \(\forall \) as \(\lnot \exists \lnot \)). In practice, implicit definability is not very frequent, so that in many concrete cases \(\mathtt {ImplDef}_{\psi _h,e_i}^{T_h}({\underline{x}},{\underline{z}})\) is trivially equivalent to \(\bot \) (in such cases, Step (2.i) above can obviously be disregarded).
×
6.1 The Necessity of the Equality Interpolating Condition
The following result shows that equality interpolating is a necessary condition for a transfer result, in the sense that it is already required for minimal combinations with signatures adding uninterpreted symbols:
Theorem 6
Let T be a convex, stably infinite, universal theory admitting a model completion and let \(\varSigma \) be a signature disjoint from the signature of T containing at least a unary predicate symbol. Then \(T\cup \mathcal {EUF}(\varSigma )\) admits a model completion iff T is equality interpolating.
Proof
The necessity can be shown by using the following argument. By Theorem 1, \(T\cup \mathcal {EUF}(\varSigma )\) has uniform quantifierfree interpolation, hence also ordinary quantifierfree interpolation. We can now apply Theorem 4 and get that T must be equality interpolating. Conversely, the sufficiency comes from Theorem 5 together with the fact that
\(\mathcal {EUF}(\varSigma )\) is trivially universal, convex, stably infinite, has a model completion [6] and is equality interpolating [2, 47].
\(\square \)
6.2 An Example of Combined Covers for the Convex Case
We now analyze an example in detail. Our results apply for instance to the case where \(T_1\) is \(\mathcal {EUF}(\varSigma )\) and \(T_2\) is linear real arithmetic. By ‘linear real arithmetic’ we mean the set of sentences which are true in the reals under the natural interpretation of the symbols, in the language containing \(+,,0,1,<, =\) and also infinitely many unary division operations by positive integer coefficients. This theory can be axiomatized as the theory of totally ordered abelian groups with the divisibility axiom \(n\cdot (x/n)=x\) and with \(0\ne 1\) (last axiom excludes degeneracy); this axiomatization is universal and ensures quantifier elimination (hence also the equality interpolating property, see [2] [Theorem 4.4]). This theory is also convex: actually convexity comes from the geometric fact that if a convex set is included in a finite nonempty union of hyperplanes, then it is contained in one of them.
We recall that covers are computed in linear real arithmetic by quantifier elimination, whereas for \(\mathcal {EUF}(\varSigma )\) one can apply the superpositionbased algorithm from [6]. Let us show that the cover of^{3}is the following formulaFormula (17) is already purified. Notice also that the variables \(e_1, e_2\) are in fact already explicitly defined (only \(e_3, e_4\) are truly existential variables).
$$\begin{aligned} \exists e_1\cdots \exists e_4\; ~ \left( \begin{aligned}&e_1= f(x_1)\;\wedge \; e_2= f(x_2)\; \wedge \; \\&\wedge \, f(e_3)=e_3\,\wedge \, \; f(e_4)= x_1\;\wedge \\&\wedge \; x_1+e_1\le e_3\;\wedge \; e_3\le x_2+e_2\;\wedge \;e_4=x_2+e_3 \end{aligned} \right) \end{aligned}$$
(17)
$$\begin{aligned} \begin{aligned}&[x_2=0 \; \wedge \; f(x_1)=x_1 \;\wedge \; x_1 \le 0 \; \wedge \; x_1\le f(0)]~\vee ~ \\&\vee ~ [x_1+f(x_1)< x_2+f(x_2)\,\wedge \,x_2\ne 0]~\vee \\&\vee ~ \begin{bmatrix} x_2\ne 0\, \wedge \, x_1+f(x_1)= x_2+f(x_2)\, \wedge \, f(2x_2+f(x_2))=x_1\, \wedge \, \\ ~ \wedge \, f(x_1+f(x_1))= x_1+f(x_1)\end{bmatrix} \end{aligned} \end{aligned}$$
(18)
We first make the partition guessing. There is no need to involve defined variables into the partition guessing, hence we need to consider only two partitions; they are described by the following formulae:We first analyze the case of \(P_1\). The formulae \(\psi _1\) and \(\psi _2\) to which we need to apply exhaustively Step (1) and Step (2.i) of our algorithm are:We first compute the implicit definability formulae for the truly existential variables with respect to both \(T_1\) and \(T_2\).So, if we apply Step 1 we get(notice that the literal \(x_2\ne 0\) is entailed by \(\psi _2\), so we can simplify it to \(\top \) in \(\mathtt {ImplDef}_{\psi _2,e_3}^{T_2}({\underline{x}},{\underline{z}})\) and \(\mathtt {ImplDef}_{\psi _2,e_4}^{T_2}({\underline{x}},{\underline{z}})\)). If we apply Step (2.i) (for i=3), we get (after removing implied equalities)Step (2.i) (for i=4) gives a formula logically equivalent to (20). Notice that (20) is terminal too, because all existential variables are now explicitly defined (this is a lucky sideeffect of the fact that \(e_3\) has been moved to the defined variables). Thus the exhaustive application of Steps (1) and (2.i) is concluded.
$$\begin{aligned} P_1(e_3, e_4) ~\equiv & {} ~ e_3\ne e_4 \\ P_2(e_3, e_4) ~\equiv & {} ~ e_3= e_4 \end{aligned}$$
$$\begin{aligned} \psi _1 ~\equiv & {} ~f(e_3)=e_3\,\wedge \, \; f(e_4)= x_1\;\wedge \; e_3\ne e_4 \\ \psi _2 ~\equiv & {} ~x_1+e_1\le e_3\;\wedge \; e_3\le x_2+e_2\;\wedge \;e_4=x_2+e_3\; \wedge \; e_3\ne e_4 \end{aligned}$$

We first consider \(\mathtt {ImplDef}_{\psi _1,e_3}^{T_1}({\underline{x}},{\underline{z}})\). Here we show that the cover of the negation of formula (8) is equivalent to \(\top \) (so that \(\mathtt {ImplDef}_{\psi _1,e_3}^{T_1}({\underline{x}},{\underline{z}})\) is equivalent to \(\bot \)). We must quantify over truly existential variables and their duplications, thus we need to compute the cover ofThis is a saturated set according to the superposition based procedure of [6], hence the result is \(\top \), as claimed.$$\begin{aligned} f(e'_3)=e'_3\wedge f(e_3)=e_3\wedge f(e'_4)=x_1\wedge f(e_4)=x_1\wedge e_3\ne e_4 \wedge e'_3 \ne e'_4\wedge e'_3\ne e_3 \end{aligned}$$

The formula \(\mathtt {ImplDef}_{\psi _1,e_4}^{T_1}({\underline{x}},{\underline{z}})\) is also equivalent to \(\bot \), by the same argument as above.

To compute \(\mathtt {ImplDef}_{\psi _2,e_3}^{T_2}({\underline{x}},{\underline{z}})\) we use FourierMotzkin quantifier elimination. We need to eliminate the variables \(e_3, e'_3, e_4, e'_4\) (intended as existentially quantified variables) fromThis gives \(x_1+e_1\ne x_2+e_2 \wedge x_2\ne 0\), so that \(\mathtt {ImplDef}_{\psi _2,e_3}^{T_2}({\underline{x}},{\underline{z}})\) is \(x_1+e_1= x_2+e_2 \wedge x_2\ne 0\). The corresponding equality interpolating term for \(e_3\) is \(x_1+e_1\).$$\begin{aligned} \begin{aligned}&x_1+e_1\le e'_3\le x_2+e_2\wedge x_1+e_1\le e_3\le x_2+e_2\wedge e'_4=x_2+e'_3\wedge \\&\wedge e_4=x_2+e_3 \wedge e_3\ne e_4 \wedge e'_3 \ne e'_4\wedge e'_3\ne e_3~~. \end{aligned} \end{aligned}$$

The formula \(\mathtt {ImplDef}_{\psi _2,e_4}^{T_2}({\underline{x}},{\underline{z}})\) is also equivalent to \(x_1+e_1= x_2+e_2\wedge x_2\ne 0\) and the equality interpolating term for \(e_4\) is \(x_1+e_1+x_2\).
$$\begin{aligned} \exists e_1\cdots \exists e_4 \left( \begin{aligned}&e_1= f(x_1)\;\wedge \; e_2=f(x_2)\; \wedge \\&\wedge \, f(e_3)=e_3\,\wedge \, \; f(e_4)= x_1\;\wedge \; e_3\ne e_4\;\wedge \\&\wedge \, x_1+e_1\le e_3\,\wedge \, e_3\le x_2+e_2\,\wedge \, e_4=x_2+e_3 \, \wedge \, x_1+e_1\ne x_2+e_2 \end{aligned} \right) \end{aligned}$$
(19)
$$\begin{aligned} \exists e_1\cdots \exists e_4\; ~ \left( \begin{aligned}&e_1=f(x_1)\;\wedge \; e_2=f(x_2)\; \wedge \; e_3=x_1+e_1 \;\wedge \\&\wedge \, f(e_3)=e_3\,\wedge \, \; f(e_4)= x_1\;\wedge \; e_3\ne e_4\;\wedge \\&\wedge \; e_4=x_2+e_3 \;\wedge \; x_1+e_1= x_2+e_2 \end{aligned} \right) \end{aligned}$$
(20)
Applying the final step of Proposition 2 to (20) is quite easy: it is sufficient to unravel the acyclic definitions. The result, after little simplification, isthis can be further simplified toAs to formula (19), we need to apply the final cover computations mentioned in Proposition 2. The formulae \(\psi _1\) and \(\psi _2\) are nowThe \(T_1\)cover of \(\psi _1'\) is \(\top \). For the \(T_2\)cover of \(\psi _2'\), eliminating with FourierMotzkin the variables \(e_4\) and \(e_3\), we getwhich becomesafter unravelling the explicit definitions of \(e_1, e_2\). Thus, the analysis of the case of the partition \(P_1\) gives, as a result, the disjunction of (21) and (22).
$$\begin{aligned} \begin{aligned}&x_2\ne 0\, \wedge \, x_1+f(x_1)= x_2+f(x_2)\, \wedge \, \\&\wedge \, f(x_2+f(x_1+f(x_1)))=x_1\, \wedge \, f(x_1+f(x_1))= x_1+f(x_1); \end{aligned} \end{aligned}$$
$$\begin{aligned} \begin{aligned}&x_2\ne 0\, \wedge \, x_1+f(x_1)= x_2+f(x_2)\, \wedge \\&\wedge \, f(2x_2+f(x_2))=x_1\, \wedge \, f(x_1+f(x_1))= x_1+f(x_1); \end{aligned} \end{aligned}$$
(21)
$$\begin{aligned} \psi '_1~\equiv ~&f(e_3)=e_3\;\wedge \, \; f(e_4)= x_1\;\wedge \, \; e_3\ne e_4~~~~~~~~~~~~~~~~ \\ \psi '_2~\equiv ~&x_1+e_1\le e_3 \le x_2+e_2\,\wedge \, e_4=x_2+e_3 \, \wedge \, x_1+e_1\ne x_2+e_2\;\wedge \; e_3\ne e_4 \end{aligned}$$
$$\begin{aligned} x_1+e_1< x_2+e_2\,\wedge \,x_2\ne 0 \end{aligned}$$
$$\begin{aligned} x_1+f(x_1)< x_2+f(x_2)\,\wedge \,x_2\ne 0 \end{aligned}$$
(22)
We now analyze the case of \(P_2\). Before proceeding, we replace \(e_4\) with \(e_3\) (since \(P_2\) precisely asserts that these two variables coincide); our formulae \(\psi _1\) and \(\psi _2\) becomeFrom \(\psi ''_1\) we deduce \(e_3=x_1\), thus we can move \(e_3\) to the explicitly defined variables (this avoids useless calculations: the implicit definability condition for variables having an entailed explicit definition is obviously \(\top \), so making case split on it produces either tautological consequences or inconsistencies). In this way we get the terminal working formulaUnravelling the explicit definitions, we get (after exhaustive simplifications)Now, the disjunction of (21), (22) and (24) is precisely the final result (18) claimed above. This concludes our detailed analysis of our example.
$$\begin{aligned} \psi ''_1 ~\equiv & {} ~f(e_3)=e_3\,\wedge \, \; f(e_3)= x_1 \\ \psi ''_2 ~\equiv & {} ~x_1+e_1\le e_3\;\wedge \; e_3\le x_2+e_2\;\wedge \;0=x_2\; \end{aligned}$$
$$\begin{aligned} \exists e_1\cdots \exists e_3 \left( \begin{aligned}&e_1= f(x_1)\;\wedge \; e_2=f(x_2)\; \wedge \; e_3=x_1 \\&\wedge \, f(e_3)=e_3\,\wedge \, \; f(e_3)= x_1\;\wedge \; \\&\wedge \, x_1+e_1\le e_3\,\wedge \, e_3\le x_2+e_2\,\wedge \, 0=x_2 \end{aligned} \right) \end{aligned}$$
(23)
$$\begin{aligned} x_2=0 \; \wedge \; f(x_1)=x_1 \;\wedge \; x_1 \le 0 \; \wedge \; x_1\le f(0) \end{aligned}$$
(24)
Notice that the example shows that combined cover computations may introduce terms with arbitrary alternations of symbols from both theories (like \(f(x_2+f(x_1+f(x_1)))\) above). The point is that when a variable becomes explicitly definable via a term in one of the theories, then using such additional variable may in turn cause some other variables to become explicitly definable via terms from the other theory, and so on and so forth; when ultimately the explicit definitions are unraveled, highly nested terms arise with many symbol alternations from both theories.
7 The Nonconvex Case: A Counterexample
In this section, we show by giving a suitable counterexample that the convexity hypothesis cannot be dropped from Theorems 5, 6. We make use of basic facts about ultrapowers (see [11] for the essential information we need). We take as \(T_1\) integer difference logic \(\mathcal {IDL}\), i.e. the theory of integer numbers under the unary operations of successor and predecessor, the constant 0 and the strict order relation <. This is stably infinite, universal and has quantifier elimination (thus it coincides with its own model completion). It is not convex, but it satisfies the equality interpolating condition, once the latter is suitably adjusted to nonconvex theories, see [2] for the related definition and all the above mentioned facts.
As \(T_2\), we take \(\mathcal {EUF}(\varSigma _{f})\), where \(\varSigma _f\) has just one unary free function symbol f (this f is supposed not to belong to the signature of \(T_1\)).
Proposition 3
Let \(T_1, T_2\) be as above; the formuladoes not have a cover in \(T_1\cup T_2\).
$$\begin{aligned} \exists e\;(0<e \wedge e< x\wedge f(e)=0) \end{aligned}$$
(25)
Proof
Suppose that (25) has a cover \(\phi (x)\). This means (according to CoverbyExtensions Lemma 1) that for every model \(\mathcal {M}\) of \(T_1\cup T_2\) and for every element \(a\in \vert \mathcal {M}\vert \) such that \(\mathcal {M}\models \phi (a)\), there is an extension \(\mathcal {N}\) of \(\mathcal {M}\) such that \(\mathcal {N}\models \exists e\;(0<e \wedge e< a\wedge f(e)=0)\).
Consider the model \(\mathcal {M}\), so specified: the support of \(\mathcal {M}\) is the set of the integers, the symbols from the signature of \(T_1\) are interpreted in the standard way and the symbol f is interpreted so that 0 is not in the image of f. Let \(a_k\) be the number \(k>0\) (it is an element from the support of \(\mathcal {M}\)). Clearly it is not possible to extend \(\mathcal {M}\) so that \(\exists e\;(0<e \wedge e< a_k\wedge f(e)=0)\) becomes true: indeed, we know that all the elements in the interval (0, k) are definable as iterated successors of 0 and, by using the axioms of \(\mathcal {IDL}\), no element can be added between a number and its successor, hence this interval cannot be enlarged in a superstructure. We conclude that \(\mathcal {M}\models \lnot \phi (a_k)\) for every k.
Consider now an ultrapower \(\prod _D \mathcal {M}\) of \(\mathcal {M}\) modulo a nonprincipal ultrafilter D and let a be the equivalence class of the tuple \(\langle a_k\rangle _{k\in {\mathbb {N}}}\); by the fundamental Los theorem [11], \(\prod _D \mathcal {M}\models \lnot \phi (a)\). We claim that it is possible to extend \(\prod _D {\mathcal {M}}\) to a superstructure \({\mathcal {N}}\) such that \(\mathcal {N}\models \exists e\;(0<e \wedge e< a\wedge f(e)=0)\): this would entail, by definition of cover, that \(\prod _D {\mathcal {M}}\models \phi (a)\), contradiction. We now show why the claim is true. Indeed, since \(\langle a_k\rangle _{k\in {\mathbb {N}}}\) has arbitrarily big numbers as its components, we have that, in \(\prod _D \mathcal {M}\), a is bigger than all standard numbers.
Thus, if we take a further nonprincipal ultrapower \(\mathcal {N}\) of \(\prod _D \mathcal {M}\), it becomes possible to change in it the evaluation of f(b) for some \(b<a\) and set it to 0 (in fact, as it can be easily seen,
there are elements \(b\in \vert \mathcal {N}\vert \) less than a but not in the support of \(\prod _D \mathcal {M}\)). \(\square \)
The counterexample still applies when replacing integer difference logic with linear integer arithmetics (the proof is literally the same).
8 Tame Combinations
So far, we only analyzed the monosorted case. However, many interesting examples arising in modelchecking verification are multisorted: this is the case of arraybased systems [20] and in particular of the arraybased system used in dataaware processes verification [5, 9]. The above examples suggest restrictions on the theories to be combined other than convexity, in particular they suggest restrictions that make sense in a multisorted context.
Most definitions we gave in Sect. 2 have straightforward natural extensions to the multisorted case (we leave the reader to formulate them). A little care is needed however for the disjoint signatures requirement. Let \(T_1, T_2\) be multisorted theories in the signatures \(\varSigma _1, \varSigma _2\); the disjointness requirement for \(\varSigma _1\) and \(\varSigma _2\) can be formulated in this context by saying that the only function or relation symbols in \(\varSigma _1\cap \varSigma _2\) are the equality predicates over the common sorts in \(\varSigma _1\cap \varSigma _2\). We want to strengthen this requirement: we say that the combination \(T_1\cup T_2\) is tame iff the sorts in \(\varSigma _1\cap \varSigma _2\) cannot be a domain sort of a symbol from \(\varSigma _1\) other than an equality predicate. In other words, if a relation or a function symbol has as among its domain sorts a sort from \(\varSigma _1\cap \varSigma _2\), then this symbol is from \(\varSigma _2\) (and not from \(\varSigma _1\), unless it is the equality predicate).
Tame combinations arise in infinitestate modelchecking (in fact, the definition is suggested by this application domain), where signatures can be split into a signature \(\varSigma _2\) used to represent ‘datatypes’ like integers and a signature \(\varSigma _1\) for representing elements contained in a database: this is customary in the literature on dataaware processes verification [5, 9].
Notice that the notion of a tame combination is not symmetric in \(T_1\) and \(T_2\): to see this, notice that if the sorts of \(\varSigma _1\) are included in the sorts of \(\varSigma _2\), then \(T_1\) must be a pure equality theory (but this is not the case if we swap \(T_1\) with \(T_2\)). The combination of \(\mathcal {IDL}\) and \(\mathcal {EUF}(\varSigma )\) used in the counterexample of Sect. 7 is not tame: even if we formulate \(\mathcal {EUF}(\varSigma )\) as a twosorted theory, the unique sort of \(\mathcal {IDL}\) must be a sort of \(\mathcal {EUF}(\varSigma )\) too, as witnessed by the impure atom \(f(e)=0\) in the formula (25). Because of this, for the combination to be tame, \(\mathcal {IDL}\) should play the role of \(T_2\) (the arithmetic operation symbols are defined on a shared sort); however, the unary function symbol \(f\in \varSigma \) has a shared sort as domain sort, so the combination is not tame anyway.
In a tame combination, an atomic formula A can only be of two kinds: (1) we say that A is of the first kind iff the sorts of its root predicate are from \(\varSigma _1\setminus \varSigma _2\); (2) we say that A is of the second kind iff the sorts of its root predicate are from \(\varSigma _2\). We use the roman letters \(e, x,\dots \) for variables ranging over sorts in \(\varSigma _1\setminus \varSigma _2\) and the greek letters \(\eta , \xi , \dots \) for variables ranging over sorts in \(\varSigma _2\). Thus, if we want to display free variables, atoms of the first kind can be represented as \(A(e,x, \dots )\), whereas atoms of the second kind can be represented as \(A(\eta , \xi , \dots , t(e, x, \dots ), \dots )\), where the t are \(\varSigma _1\)terms. In the following, given two tuples of \(\varSigma _i\)terms \(\underline{\alpha }:=\langle \alpha _1,\ldots ,\alpha _n\rangle \) and \(\underline{\beta }:=\langle \beta _1,\ldots ,\beta _n\rangle \) (for some \(i=1,2\)), we use the notation \(\underline{\alpha }=\underline{\beta }\) for denoting the conjunction of equalities \(\bigwedge _j \alpha _j = \beta _j\).
Remark 2
We remark that if a formula \(\psi ({\underline{\eta }})\) is a \(\varSigma _1\)formula and \({\underline{\eta }}\) are variables of \(\varSigma _2\)sorts, according to the definition of a tame combination, \(\psi ({\underline{\eta }})\) must be a conjunction of equalities and disequalities between variables: indeed, in this case \({\underline{\eta }}\) need to range over the interpretation of a common sort S, and \(\psi \) cannot contain nonvariable terms built out of \({\underline{\eta }}\), because there cannot be a \(\varSigma _1\)function symbol having S as domain.
Suppose that \(T_1\cup T_2\) is a tame combination and that \(T_1, T_2\) are universal theories admitting model completions \(T_1^*, T_2^*\). We propose the following algorithm, called \(\mathsf {TameCombCover}\), to compute the cover of a primitive formula; this formula must be of the kindwhere \(\phi \) is a \(\varSigma _1\)conjunction of literals, \(\psi \) is a conjunction of \(\varSigma _2\)literals and the \({\underline{t}}\) are \(\varSigma _1\)terms.
$$\begin{aligned} \exists {\underline{e}}\;\exists {\underline{\eta }}(\phi ({\underline{e}}, {\underline{x}}) \wedge \psi ({\underline{\eta }}, {\underline{\xi }}, {\underline{t}}({\underline{e}},{\underline{x}}))) \end{aligned}$$
(26)
The \(\mathsf {TameCombCover}\) algorithm has three steps: We now show that the above algorithm is correct under very mild hypotheses. We need some technical facts about stably infinite theories in a multisorted context. We say that a multisorted theory T is stably infinite with respect to a set of sorts \(\mathcal {S}\) from its signature iff every Tsatisfiable constraint is satisfiable in a model \(\mathcal {M}\) where, for every \(S\in \mathcal {S}\), the set \(S^\mathcal {M}\) (namely the interpretation of the sort S in \(\mathcal {M}\)) is infinite. The next Lemma is a light generalization of Lemma 2 and is proved in the same way:
(i)
We flatten (26) and get where the \({\underline{\eta }}'\) are fresh variables abstracting out the \({\underline{t}}\) and \({\underline{\eta }}'= {\underline{t}}({\underline{e}}, {\underline{x}})\) is a componentwise conjunction of equalities.
$$\begin{aligned} \exists {\underline{e}}\;\exists {\underline{\eta }}\; \exists {\underline{\eta }}'\; (\phi ({\underline{e}}, {\underline{x}}) \wedge {\underline{\eta }}'= {\underline{t}}({\underline{e}}, {\underline{x}})\wedge \psi ({\underline{\eta }}, {\underline{\xi }}, {\underline{\eta }}'))) \end{aligned}$$
(27)
(ii)
We apply the cover algorithm of \(T_1\) to the formula this gives as a result a formula \({\tilde{\phi }}({\underline{x}}, {\underline{\eta }}')\) that we put in DNF. A disjunct of \({\tilde{\phi }}\) will have the form \(\phi _1({\underline{x}})\wedge \phi _2({\underline{\eta }}', {\underline{t}}'({\underline{x}}))\) after separation of the literals of the first and of the second kind. We pick such a disjunct \(\phi _1({\underline{x}})\wedge \phi _2({\underline{\eta }}', {\underline{t}}'({\underline{x}}))\) of the DNF of \({\tilde{\phi }}({\underline{x}}, {\underline{\eta }}')\) and update our current primitive formula to (this step is nondeterministic: in the end we shall output the disjunction of all possible outcomes). Here again the \({\underline{\xi }}'\) are fresh variables abstracting out the terms \({\underline{t}}'\).^{4}
$$\begin{aligned} \exists {\underline{e}}\; (\phi ({\underline{e}}, {\underline{x}}) \wedge {\underline{\eta }}'= {\underline{t}}({\underline{e}}, {\underline{x}}))~~; \end{aligned}$$
(28)
$$\begin{aligned} \exists {\underline{\xi }}'\;({\underline{\xi }}'= {\underline{t}}'({\underline{x}})\wedge (\exists {\underline{\eta }}\; \exists {\underline{\eta }}'\; (\phi _1({\underline{x}})\wedge \phi _2({\underline{\eta }}', {\underline{\xi }}') \wedge \psi ({\underline{\eta }}, {\underline{\xi }}, {\underline{\eta }}')))) \end{aligned}$$
(29)
(iii)
We apply the cover algorithm of \(T_2\) to the formula this gives as a result a formula \(\psi '({\underline{\xi }}, {\underline{\xi }}')\). We update our current formula to and finally to the equivalent quantifierfree formula
$$\begin{aligned} \exists {\underline{\eta }}\; \exists {\underline{\eta }}'\; (\phi _2({\underline{\eta }}', {\underline{\xi }}') \wedge \psi ({\underline{\eta }}, {\underline{\xi }}, {\underline{\eta }}')) \end{aligned}$$
(30)
$$\begin{aligned} \exists {\underline{\xi }}'\;({\underline{\xi }}'= {\underline{t}}'({\underline{x}})\wedge \phi _1({\underline{x}})\wedge \psi '( {\underline{\xi }}, {\underline{\xi }}' )) \end{aligned}$$
$$\begin{aligned} \phi _1({\underline{x}})\wedge \psi '( {\underline{\xi }}, {\underline{t}}'({\underline{x}}) ). \end{aligned}$$
(31)
Lemma 7
Let T be stably infinite with respect to a subset \(\mathcal {S}\) of the set of sorts of the signature of T. Let \(\mathcal {M}\) be a model of T and let, for every \(S\in \mathcal {S}\), \(X_S\) be an at most countable superset of \(S^\mathcal {M}\). Then there is an extension \(\mathcal {N}\) of \(\mathcal {M}\) such that for all \(S\in \mathcal {S}\) we have \(S^\mathcal {N}\supseteq X_S\).
Proof
Let us expand the signature of T with the set C of fresh constants (we take one constant for every \(c\in X_S\setminus S^\mathcal {M}\)). We need to prove the Tconsistency of \(\varDelta (\mathcal {M})\) with a the set D of disequalities asserting that all \(c\in C\) are different from each other and from the names of the elements of the support of \(\mathcal {M}\). By compactness, it is sufficient to ensure the Tconsistency of \(\varDelta _0 \cup D_0\), where \(\varDelta _0\) and \( D_0\) are finite subsets of \( \varDelta (\mathcal {M})\) and D, respectively. Since \(\mathcal {M}\models \varDelta _0\), this set is Tconsistent and hence it is satisfied in a Tmodel \(\mathcal {M}'\) where all the sorts in \(\mathcal {S}\) are interpreted as infinite sets; in such \(\mathcal {M}'\), it is trivially seen that we can interpret also the constants occurring in \(D_0\) so as to make \(D_0\) true too. \(\square \)
Lemma 8
Let \(T_1, T_2\) be universal signature disjoint theories which are stably infinite with respect to the set of shared sorts (we let \(\varSigma _1\) be the signature of \(T_1\) and \(\varSigma _2\) be the signature of \(T_2\)). Let the index i be 1 or 2: we let \(\mathcal {M}_0\) be a model of \(T_1\cup T_2\) and \(\mathcal {M}_1\) be a model of \(T_i\) extending the \(\varSigma _i\)reduct of \(\mathcal {M}_0\). Then there exists a model \(\mathcal {N}\) of \(T_1\cup T_2\), extending \(\mathcal {M}_0\) as a \(\varSigma _1\cup \varSigma _2\)structure and whose \(\varSigma _i\)reduct extends \(\mathcal {M}_1\).
Proof
Using Lemma 7, we build infinitely many models \(\mathcal {M}_0,\mathcal {M}_1, \mathcal {M}_2,\dots \) such that: (i) \(\mathcal {M}_{2j}\) is a \(\varSigma _{3i}\)structure which is a model of \(T_{3i}\); (ii) \(\mathcal {M}_{2j+1}\) is a \(\varSigma _{i}\)structure which is a model of \(T_i\); (iii) \(\mathcal {M}_{2j+2}\) is a \(\varSigma _{3i}\)extension of \(\mathcal {M}_{2j}\); (iv) \(\mathcal {M}_{2j+3}\) is a \(\varSigma _{i}\)extension of \(\mathcal {M}_{2j+1}\); (v) the supports of the \(\mathcal {M}_k\), once restricted to the \(\varSigma _1\cap \varSigma _2\)sorts (call \(\vert \mathcal {M}_k\vert \) such restrictions), form an increasing chain \(\vert \mathcal {M}_0\vert \subseteq \vert \mathcal {M}_1\vert \subseteq \vert \mathcal {M}_2\vert \subseteq \cdots \).
The union over this chain of models will be the desired \(\mathcal {N}\). \(\square \)
We are now ready for the main result of this section:
Theorem 7
Let \(T_1\cup T_2\) be a tame combination of two universal theories admitting a model completion. If \(T_1,T_2\) are also stably infinite with respect to their shared sorts, then \(T_1\cup T_2\) has a model completion. Covers in \(T_1\cup T_2\) can be computed as shown in the above threesteps algorithm \(\mathsf {TameCombCover}\).
Proof
Since condition (i) of Lemma 1 is trivially true, we need only to check condition (ii), namely that given a \(T_1\cup T_2\)model \(\mathcal {M}\) and elements \({\underline{a}}, {\underline{b}}\) from its support such that \(\mathcal {M}\models \phi _1({\underline{a}})\wedge \psi '( {\underline{b}}, {\underline{t}}'({\underline{a}}) )\) as in (31), then there is an extension \(\mathcal {N}\) of \(\mathcal {M}\) such that (26) is true in \(\mathcal {N}\) when evaluating \({\underline{x}}\) over \({\underline{a}}\) and \({\underline{\xi }}\) over \({\underline{b}}\).
If we let \({\underline{b}}'\) be the tuple such that \(\mathcal {M}\models {\underline{b}}'= {\underline{t}}'({\underline{a}})\), then we have \(\mathcal {M}\models {\underline{b}}'= {\underline{t}}'({\underline{a}})\wedge \phi '({\underline{a}})\wedge \psi '( {\underline{b}}, {\underline{b}}' )\). Since \(\psi '({\underline{\xi }}, {\underline{\xi }}')\) is the \(T_2\)cover of (30), the \(\varSigma _2\)reduct of \(\mathcal {M}\) embeds into a \(T_2\)model where (30) is true under the evaluation of the \({\underline{\xi }}\) as the \({\underline{b}}\). By Lemma 8, this model can be embedded into a \(T_1\cup T_2\)model \(\mathcal {M}'\) in such a way that \(\mathcal {M}'\) is an extension of \(\mathcal {M}\) and that \(\mathcal {M}'\models {\underline{b}}'= {\underline{t}}'({\underline{a}})\wedge \phi _1({\underline{a}})\wedge \phi _2({\underline{c}}', {\underline{b}}') \wedge \psi ({\underline{c}}, {\underline{b}}, {\underline{c}}')\) holds for some \({\underline{c}}, {\underline{c}}'\). Since \(\phi _1({\underline{x}})\wedge \phi _2({\underline{\eta }}', {\underline{t}}'({\underline{x}}))\) implies the \(T_1\)cover of (28) and \(\mathcal {M}'\models \phi _1({\underline{a}})\wedge \phi _2({\underline{c}}', {\underline{t}}({\underline{a}}))\), then the \(\varSigma _1\)reduct of \(\mathcal {M}'\) can be extended to a \(T_1\)model where (28) is true when evaluating the \({\underline{x}}, {\underline{\eta }}'\) to the \({\underline{a}}, {\underline{c}}'\). Again by Lemma 8, this model can be extended to a \(T_1\cup T_2\)model \(\mathcal {N}\) such that \(\mathcal {N}\) is an extension of \(\mathcal {M}'\) (hence also of \(\mathcal {M}\)) and \(\mathcal {N}\models \phi ({\underline{a}}', {\underline{a}}) \wedge {\underline{c}}'= {\underline{t}}({\underline{a}}', {\underline{a}})\wedge \psi ({\underline{c}}, {\underline{b}}, {\underline{c}}') \), that is \(\mathcal {N}\models \phi ({\underline{a}}', {\underline{a}}) \wedge \psi ({\underline{c}}, {\underline{b}}, {\underline{t}}({\underline{a}}', {\underline{a}})) \). This means that \(\mathcal {N}\models \exists {\underline{e}}\;\exists {\underline{\eta }}(\phi ({\underline{e}}, {\underline{a}}) \wedge \psi ({\underline{\eta }}, {\underline{b}},{\underline{t}}({\underline{e}},{\underline{a}}))) \), as desired. \(\square \)
We conclude this subsection discussing the applications that inspired tame combinations. In the context of dataaware processes verification [4, 5, 9], where relational databases can be extended with arithmetical values such as integers and reals, tame combinations become particularly interesting. Consider the combination \(T_{DB}\cup T_{int}\), where: It can be trivially seen that this combination is tame.
1.
\(T_{DB}\) is a multisorted version of \(\mathcal {EUF}(\varSigma )\) in a signature \(\varSigma \) comprising three sorts \(\mathcal {S}_1,\mathcal {S}_2,\mathcal {S}_3\), and two function symbols \(f_{R,1}:\mathcal {S}_1\rightarrow \mathcal {S}_2\) and \(f_{R,2}:\mathcal {S}_1\rightarrow \mathcal {S}_3\);
2.
\(T_{int}\) is some theory for linear arithmetics, e.g., \(\mathcal {LIA} \) or \(\mathcal {LRA}\), such that the unique sort of \(T_{int}\) coincides with \(\mathcal {S}_3\).
As explained in [9], \((\varSigma , T_{DB})\) can be thought of as a DB schema, i.e. as the formalization of a classical relational database with primary and foreign keys: for instance, from unary functions \(f_{R,1}\) and \(f_{R,2}\), one can reconstruct the corresponding database relation \(R(A_1,A_2,A_3)\), where each attribute \(A_i\) has type \(\mathcal {S}_i\) (for \(i=1,\ldots ,3\)) and \(A_1\) is the primary key of R. The interested reader is referred to [9, 31] for details on this. In addition, \(\mathcal {S}_3\), which is interpreted into a model of \(T_{int}\), can be used to formalize a value domain (using again the nomenclature of [9]), i.e., an infinite arithmetic domain whose elements are constrained by \(T_{int}\): in this sense, these elements can be thought of as (possibly infinitely many and fresh) values that can be injected into the database, e.g., by an external user (they are essential for applications in dataaware process verification). For details on this and its use in formal verification, see [31].
8.1 An Example of Combined Covers for the Tame Combination
Let \(T_1\) be \(\mathcal {EUF}(\varSigma _1)\), where \(\varSigma _1\) is a multisorted signature with three sorts \(\mathcal {S}_1\), \(\mathcal {S}_2\) and \(\mathcal {S}_3\) and with a function symbol \(f: \mathcal {S}_1\times \mathcal {S}_2\rightarrow \mathcal {S}_3\). Let \(T_2\) be \(\mathcal {LIA} \) (which is not convex, see [2, Sect. 4] for a precise description of this theory), where its (unique) sort is \(\mathcal {S}_3\), which is in common with \(\varSigma _1\). We notice that \(T_1\cup T_2\) is a tame combination, since the common sort \(\mathcal {S}_3\) is the codomain sort (and not the domain sort) of the unique symbol f from \(\varSigma _1\) different from equality. We show a simple example on how to compute a \(T_1\cup T_2\)cover using the above algorithm.
Letbe the formula for which we would like to compute a \(T_1\cup T_2\)cover: the only truly existentially quantified variable here is e.
$$\begin{aligned} \exists e \left( \begin{aligned}&f(e,x_1) \le f(e,x_2) \wedge 2\xi _2 \le f(e,x_1)+\xi _1 \\&\wedge f(e,x_2)+\xi _3< 4\xi _4 \wedge \xi _3\le \xi _1 \end{aligned} \right) \end{aligned}$$
(32)
We first apply the First Step, and we abstract out \(f(e,x_1)\) and \(f(e,x_2)\) by introducing two fresh variables \(\eta '_1\) and \(\eta '_2\):Then, in order to apply the Second Step, we need to compute the \(T_1\)cover of the following formula:and we obtain:which, in turn, is equivalent to the following formula in DNF form:Now, we analyze the two different cases create by each disjunct in the previous formula.
$$\begin{aligned} \exists e,\eta '_1,\eta '_2 \left( \begin{aligned}&\eta '_1= f(e,x_1)~\wedge ~ \eta '_2= f(e,x_2) ~ \wedge ~ 2\xi _2 \le \eta '_1+\xi _1 \\&\wedge ~\eta '_2+\xi _3< 4\xi _4 ~\wedge ~ \xi _3\le \xi _1 ~\wedge \eta '_1 \le \eta '_2 \end{aligned} \right) \end{aligned}$$
(33)
$$\begin{aligned} \exists e ~(\eta '_1= f(e,x_1)~\wedge ~ \eta '_2= f(e,x_2)) \end{aligned}$$
(34)
$$\begin{aligned} x_1= x_2 \rightarrow \eta '_1=\eta '_2 \end{aligned}$$
$$\begin{aligned} x_1\ne x_2 \vee \eta '_1=\eta '_2 \end{aligned}$$
First Case If we pick up the disjunct \(x_1\ne x_2\), after updating Formula (33), we get the following equivalent formula:We now apply the Third Step, by computing the \(T_2\)cover of the formula:This is in general achieved by applying the Cooper’s algorithm [12]. In this case, it is sufficient to notice that Formula (36) implies:which provide lower and upper bounds for both \(\eta '_1\) and \(\eta '_2\), as wanted. Hence, the \(T_2\)cover of Formula (36) is:We then update our Formula (35) and we get the first disjunct of our \(T_1\cup T_2\)cover:Second Case If we pick up the disjunct \(\eta '_1=\eta '_2\), after updating Formula (33), we get the following equivalent formula:We now apply the Third Step, by computing the \(T_2\)cover of the previous formula. In this case, it is sufficient to notice that Formula (39) implies:which provide lower and upper bounds for both \(\eta '_1\) and \(\eta '_2\), as wanted. Hence, the \(T_2\)cover of Formula (39) is:We then update our Formula (39) and we get the second disjunct of our \(T_1\cup T_2\)cover:Hence, by taking the disjunction of Formulae (38) and (41) it is straightforward to see that the \(T_1\cup T_2\)cover of Formula (32) is equivalent to:
$$\begin{aligned} \exists \eta '_1,\eta '_2 \left( \begin{aligned}&x_1\ne x_2 \wedge 2\xi _2 \le \eta '_1+\xi _1 ~\wedge ~ \eta '_2+\xi _3 \le 1+ 4\xi _4 \\&~\wedge ~ \xi _3\le \xi _1 ~\wedge ~ \eta '_1\le \eta '_2 \end{aligned} \right) \end{aligned}$$
(35)
$$\begin{aligned} \exists \eta '_1,\eta '_2 \left( \begin{aligned}&2\xi _2 \le \eta '_1+\xi _1 ~\wedge ~ \eta '_2+\xi _3\le 1+ 4\xi _4 \\&~\wedge ~ \xi _3\le \xi _1 ~\wedge ~ \eta '_1 \le \eta '_2 . \end{aligned} \right) \end{aligned}$$
(36)
$$\begin{aligned} 2\xi _2\xi _1 \le \eta '_1 ~~\wedge ~~ \eta '_1\le \eta '_2 ~~\wedge ~~ \eta '_2\le 1+ 4\xi _4\xi _3 \end{aligned}$$
$$\begin{aligned} 2\xi _2\xi _1\le 1+ 4\xi _4\xi _3~\wedge ~\xi _3\le \xi _1 \end{aligned}$$
(37)
$$\begin{aligned} x_1\ne x_2 ~\wedge ~2\xi _2\xi _1\le 1+4\xi _4\xi _3~\wedge ~\xi _3\le \xi _1 \end{aligned}$$
(38)
$$\begin{aligned} \exists \eta '_1,\eta '_2 \left( \begin{aligned}&\eta '_1=\eta '_2 \wedge 2\xi _2 \le \eta '_1+\xi _1 ~\wedge ~ \eta '_2+\xi _3\le 1+4\xi _4 \\&~\wedge ~ \xi _3\le \xi _1 ~\wedge ~ \eta '_1 \le \eta '_2 \end{aligned} \right) \end{aligned}$$
(39)
$$\begin{aligned} 2\xi _2\xi _1 \le \eta '_1 ~~\wedge ~~ \eta '_1= \eta '_2 ~~\wedge ~~ \eta '_2\le 1+ 4\xi _4\xi _3 \end{aligned}$$
$$\begin{aligned} 2\xi _2\xi _1\le 1+ 4\xi _4\xi _3~\wedge ~\xi _3\le \xi _1 \end{aligned}$$
(40)
$$\begin{aligned} 2\xi _2\xi _1\le 1+ 4\xi _4\xi _3~\wedge ~\xi _3\le \xi _1 \end{aligned}$$
(41)
$$\begin{aligned} 2\xi _2\xi _1\le 1+ 4\xi _4\xi _3~\wedge ~\xi _3\le \xi _{1} \end{aligned}$$
(42)
9 Conclusions and Future Work
In this paper we showed that covers (aka uniform interpolants) exist in the combination of two convex universal theories over disjoint signatures in case they exist in the component theories and in case the component theories also satisfy the equality interpolating condition. Notice that the last condition is needed to transfer to combinations the existence of (ordinary) quantifierfree interpolants. In order to prove our result on combined covers, Beth definability property for primitive fragments turned out to be the crucial ingredient to extensively employ. In case convexity fails, we showed by a counterexample that covers might not exist in the combined theory. The last result raises the following research problem: even if in general covers do not exist for the combination of nonconvex theories, under which conditions can one decide whether covers exist and, if so, how can one compute them?
Another interesting research question concerns complexity of the convex combined algorithm. It generates a tree whose depth is linear, hence the number of created nodes are in the worst case exponential. In order to generate new nodes, the algorithm makes use of the cover algorithms for the component theories and of the algorithms for generating the equality interpolating terms: these algorithms are given as input to our algorithm. Taking into consideration also the fact that these algorithms are used recursively, it is not immediate to give a significant upper bound to the overall complexity in the general case: instead, notice that this problem strongly depends on the component theories considered, hence it should be tackled separately for each involved theory and in view of the specific, concrete applications that the users have in mind. For these reasons, we leave an exhaustive investigation of this to future work, since it would require genuinely novel research and a thorough analysis of different examples of theories.
Applications suggested a different line of investigations, which led us to consider socalled ‘tame combinations’. In dataaware processes verification [4, 5, 9] one uses tame combinations \(T_1\cup T_2\), where \(T_1\) is a multisorted version of \(\mathcal {EUF}(\varSigma )\) in a signature \(\varSigma \) containing only unary function symbols and relation symbols of any arity, and where \(T_2\) is typically some fragment of linear arithmetics (\(T_2\)sorts are called value sorts in the terminology of [4, 5, 9]). In this context, quantifier elimination in \(T_1^*\) for primitive formulae is quadratic in complexity. Modelcheckers like MCMT represent sets of reachable states by using conjunctions of literals and during preimage computations quantifier elimination needs to be applied to primitive formulae. Now, if all relation symbols are at most binary, such a quantifier elimination in \(T_1^*\) produces conjunctions of literals out of primitive formulae. Thus, step (ii) in the algorithm from Sect. 8 becomes deterministic and the only reason why such an algorithm may become expensive (i.e., non polynomial) lies in the final quantifier elimination step for \(T_2^*\). This step might be extremely expensive if substantial arithmetic is involved, but it might still be efficiently handled in practical cases where only very limited arithmetic is used (e.g., difference bound constraints like \(xy\le n\) or \(x\le n\), where n is a constant). Our algorithm for covers in tame combinations has been implemented in version 3.0 of MCMT.
We also feel that this algorithm can be really useful in various modelchecking applications. More specifically, such a model checking framework can be applied along the recent line of research concerning analysis of dataaware processes, in which data representation and manipulation capabilities can be extended with arithmetic. Like that, one could adapt the results of this paper to the existing formalism for dataaware extensions of the defacto standard for business process modeling [4] or to dataaware classes of Petri nets [14, 15, 28, 29]. We leave it for future work.
Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.