Combined Covers and Beth Definability
 1 Citations
 224 Downloads
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 cover may not exist in the combined theories, even in case combined quantifierfree interpolants do exist.
1 Introduction
Uniform interpolants were originally studied in the context of nonclassical logics, starting from the pioneering work by Pitts [26]. We briefly 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 free in \(\phi \)), a uniform interpolant of \(\phi \) (w.r.t. \(\underline{y}\)) is a formula \(\phi '(\underline{x})\) where only the \(\underline{x}\) occur free, 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 \).
The existence of uniform interpolants is an exceptional phenomenon, which is however not so infrequent; it has been extensively studied in nonclassical logics starting from the nineties, as witnessed by a large literature (a nonexhaustive list includes [1, 11, 17, 18, 19, 23, 28, 31, 32]). 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 consequence relation but not for the global consequence relation. The connection between uniform interpolants and model completions (for equational theories axiomatizing the varieties corresponding to propositional logics) was first stated in [20] and further developed in [17, 23, 31].
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 [22]), as well as by the paper [21] by Gulwani and Musuvathi in ESOP 2008. In this last paper uniform interpolants were renamed as covers, a terminology we shall 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 [7]; 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 [15]). The usefulness of covers in model checking was already stressed in [21] and further motivated by our recent line of research on the verification of dataaware processes [5, 6, 8, 9]. Notably, it is also operationally mirrored in the MCMT [16] 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 witnessed in the comprehensive paper [29] and in related papers (e.g., [25]) 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 [6, 7, 8]. 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 fails, 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 5 below), the input cover algorithms can be suitably exploited (Proposition 1 below).
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 [14]), 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 [27] (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 [23] (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 [21] also have a combined cover algorithm for 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 [21] (but not even mentioned in their paper [21]): in fact, it was introduced by one of them some years before [33]. 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 Sect. 2, the crucial CoversbyExtensions Lemma and the relationship between covers and model completions from [7] are recalled in Sect. 3. In Sect. 4, we present some preliminary results on interpolation 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 necessary (in some sense) for combining covers. In Sect. 7 we exhibit a counteraxample to the existence of combined covers in the nonconvex case. Section 8 is devoted to the conclusions and discussion of future work. The extended version of the current paper with full proofs and details is available online in [4].
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}\). 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 set of new constants \(\bar{a}\) (the name for a), one 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}})\).
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 M\models T\) and \(\mathcal N\) is a substructure of \(\mathcal M\), then \(\mathcal N\models T\) (see [10]). 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 [10], 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 Covers and Model Completions
We report the notion of cover taken from [21] and also the basic results proved in [7]. 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 \(Res(\exists \underline{e}\, \phi )=\{\theta (\underline{y}, \underline{z})\mid T \models \phi (\underline{e}, \underline{y}) \rightarrow \theta (\underline{y}, \underline{z})\}\). 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 [7] (to be widely used throughout the paper) supplies a semantic counterpart to the notion of a cover:
Lemma 1 (CoverbyExtensions)
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})\). \(\triangleleft \)
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.
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 '\)).
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 (i) every \(\varSigma \)constraint that is satisfiable in a model of T is satisfiable in a model of \(T^*\); (ii) \(T^*\) eliminates quantifiers. Other equivalent definitions are possible [10]: 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 [10] (the latter can be seen directly or via the correspondence between quantifierfree interpolation and amalgamability, see [2]).
A close relationship between model completion and uniform interpolation emerged in the area of propositional logic (see the book [17]) and can be formulated roughly as follows. It is wellknown that most propositional calculi, via Lindembaum 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 variaties of modal agebras, 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 [17]. 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 sentences \(\forall \underline{y}\,(\psi (\underline{y}) \rightarrow \exists \underline{e}\, \phi (\underline{e}, \underline{y}))\), where \(\exists \underline{e}\, \phi (\underline{e}, \underline{y})\) is a primitive formula and \(\psi \) is a cover of it. \(\triangleleft \)
The proof (via Lemma 1, by iterating a chain construction) is in [9] (see also [3]).
4 Equality Interpolating Condition and Beth Definability
We report here some definitions and results we need concerning combined quantifierfree interpolation. Most definitions and result come from [2], but are simplified here because we restrict them to the case of universal convex theories. Further information on the semantic side is supplied in the extended version of this paper [4].
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 (see [4] for a proof):
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. \(\triangleleft \)
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, ..., 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
Theorem 2
[2, 33]. Let \(T_1\) and \(T_2\) be two universal, convex, stably infinite theories over disjoint signatures \(\varSigma _1\) and \(\varSigma _2\). If both \(T_1\) and \(T_2\) are equality interpolating and have quantifierfree interpolation property, then so does \(T_1\cup T_2\). \(\triangleleft \)
There is a converse of the previous result; for a signature \(\varSigma \), let us call \(\mathcal {EUF}(\varSigma )\) the pure equality theory over the signature \(\varSigma \) (this theory is equality interpolating and has the quantifierfree interpolation property).
Theorem 3
[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. \(\triangleleft \)
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).
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.
Theorem 4
[2]. A convex theory T having quantifierfree interpolation is equality interpolating iff it has the Beth definability property for primitive formulae. \(\triangleleft \)
Proof
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).
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})\). \(\triangleleft \)
The following Lemma supplies terms which will be used as ingredients in our combined covers algorithm:
Lemma 4
Proof
In all our concrete examples, the theory T has 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 [33]; 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. Still, an extensive investigation on te topic seems to be missed in the SMT literature.
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 shall supply a cover algorithm for \(T_1\cup T_2\) (thus proving that \(T_1\cup T_2\) has a model completion too).
Remark 1
It is not clear whether this preliminary guessing step can be avoided. In fact, NelsonOppen [24] 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. \(\triangleleft \)
In our starting formula (10), 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).
Lemma 5
Every working formula is equivalent (modulo \(T_1\cup T_2\)) to a disjunction of terminal working formulae. \(\triangleleft \)
Proof
We only sketch the proof of this Lemma (see the extended version [4] for full details), by describing the algorithm underlying it. 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 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 _1,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)^{1} is added to \(\mathtt {ExplDef}(\underline{z}, \underline{x})\); the variable \(e_i\) becomes in this way part of the defined variables.
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 we eventually terminate). \(\dashv \)
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 1
Proof
In order to show that Formula (13) is the \(T_1\cup T_2\)cover of a terminal working formula (11), we prove, by using the CoverbyExtensions Lemma 1, 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öwenheimSkolem 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 [12, 24, 30]).
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. \(\dashv \)
From Lemma 5, Proposition 1 and Theorem 1, we immediately get
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. \(\triangleleft \)
Notice that the input cover algorithms in the above combined cover computation algorithm are used not only in the final step described in Proposition 1, 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 (7) (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).
 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 (7) 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 [7], hence the result is \(\top \), as claimed.$$ 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 $$

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\).
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.
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. \(\triangleleft \)
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 3 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 [7] and is equality interpolating [2, 33]. \(\dashv \)
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 [10] 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 2
Proof
Suppose that (22) 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 \(\Pi _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 [10], \(\Pi _D \mathcal M\models \lnot \phi (a)\). We claim that it is possible to extend \(\Pi _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 \(\Pi _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 \(\Pi _D \mathcal M\), a is bigger than all standard numbers. Thus, if we take a further nonprincipal ultrapower \(\mathcal N\) of \(\Pi _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 \(\Pi _D \mathcal M\)). \(\dashv \)
The counterexample still applies when replacing integer difference logic with linear integer arithmetics.
8 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  this further condition is nevertheless needed in order to transfer the existence of (ordinary) quantifierfree interpolants. In order to prove that, 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 anymore in the combined theory. The last result raises the following research problem. Even if in general covers do not exist for combination of nonconvex theories, it would be interesting to see under what conditions one can decide whether a given cover exists and, in the affirmative case, to compute it.
Applications suggest a different line of investigations. In databasedriven verification [5, 6, 9] one uses only ‘tame’ theory combinations. A tame combination of two multisorted theories \(T_1, T_2\) in their respective signatures \(\varSigma _1, \varSigma _2\) is characterized as follows: the shared sorts can only be the codomain sort (and not 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 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). The key result for tame combination is that covers existence transfers to a tame combination \(T_1\cup T_2\) in case covers exist in the two component theories (the two component theories are only assumed to be stably infinite with respect to all shared sorts). Moreover, the transfer algorithm, in the case relevant for applications to database driven verification (where \(T_2\) is linear arithmetics and \(T_1\) is a multisorted version of \(\mathcal {EUF}(\varSigma )\) in a signature \(\varSigma \) containing only unary function symbols and relations of any arity), is relatively wellbehaved also from the complexity viewpoint because its cost is dominated by the cost of the covers computation in \(T_2\). These results on tame combinations are included in the larger ArXiv version [4] of the present paper; an implementation in the beta version 2.9 of the modelchecker MCMT is already available from the web site http://users.mat.unimi.it/users/ghilardi/mcmt.
A final future research line could consider cover transfer properties to nondisjoint signatures combinations, analogously to similar results obtained in [13, 14] for the transfer of quantifierfree interpolation.
Footnotes
References
 1.Bílková, M.: Uniform interpolation and propositional quantifiers in modal logics. Stud. Logica 85(1), 1–31 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
 2.Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifierfree interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1), 5:1–5:34 (2014)MathSciNetzbMATHCrossRefGoogle Scholar
 3.Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Quantifier elimination for database driven verification. Technical report arXiv:1806.09686, arXiv.org (2018)
 4.Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Combined covers and Beth definability (extended version). Technical report arXiv:1911.07774, arXiv.org (2019)
 5.Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Formal modeling and SMTbased parameterized verification of dataaware BPMN. In: Hildebrandt, T., van Dongen, B.F., Röglinger, M., Mendling, J. (eds.) BPM 2019. LNCS, vol. 11675, pp. 157–175. Springer, Cham (2019). https://doi.org/10.1007/9783030266196_12CrossRefGoogle Scholar
 6.Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: From model completeness to verification of data aware processes. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A.Y., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. LNCS, vol. 11560, pp. 212–239. Springer, Cham (2019). https://doi.org/10.1007/9783030221027_10zbMATHCrossRefGoogle Scholar
 7.Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 142–160. Springer, Cham (2019). https://doi.org/10.1007/9783030294366_9CrossRefGoogle Scholar
 8.Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of dataaware processes: challenges and opportunities for automated reasoning. In: Proceedings of ARCADE, EPTCS, vol. 311 (2019)Google Scholar
 9.Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: SMTbased verification of dataaware processes: a modeltheoretic approach. Math. Struct. Comput. Sci. 30(3), 271–313 (2020)MathSciNetzbMATHCrossRefGoogle Scholar
 10.Chang, C.C., Keisler, J.H.: Model Theory, 3rd edn. NorthHolland Publishing Co., Amsterdam (1990)zbMATHGoogle Scholar
 11.Ghilardi, S.: An algebraic theory of normal forms. Ann. Pure Appl. Logic 71(3), 189–245 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
 12.Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3–4), 221–249 (2004)MathSciNetzbMATHCrossRefGoogle Scholar
 13.Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (The nondisjoint signatures case). In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 316–332. Springer, Cham (2017). https://doi.org/10.1007/9783319661674_18CrossRefGoogle Scholar
 14.Ghilardi, S., Gianola, A.: Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Log. 169(8), 731–754 (2018)MathSciNetzbMATHCrossRefGoogle Scholar
 15.Ghilardi, S., Gianola, A., Kapur, D.: Compactly representing uniform interpolants for EUF using (conditional) DAGS. Technical report arXiv:2002.09784, arXiv.org (2020)
 16.Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642142031_3CrossRefGoogle Scholar
 17.Ghilardi, S., Zawadowski, M.: Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics. Trends in LogicStudia Logica Library, vol. 14. Kluwer Academic Publishers, Dordrecht (2002)Google Scholar
 18.Ghilardi, S., Zawadowski, M.W.: A sheaf representation and duality for finitely presenting heyting algebras. J. Symb. Log. 60(3), 911–939 (1995)zbMATHCrossRefGoogle Scholar
 19.Ghilardi, S., Zawadowski, M.W.: Undefinability of propositional quantifiers in the modal system S4. Stud. Logica 55(2), 259–271 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
 20.Ghilardi, S., Zawadowski, M.W.: Model completions, rHeyting categories. Ann. Pure Appl. Log. 88(1), 27–46 (1997)MathSciNetzbMATHCrossRefGoogle Scholar
 21.Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 193–207. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540787396_16zbMATHCrossRefGoogle Scholar
 22.Kapur, D.: Nonlinear polynomials, interpolants and invariant generation for system analysis. In: Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation CoLocated with ISSAC (2017)Google Scholar
 23.Kowalski, T., Metcalfe, G.: Uniform interpolation and coherence. Ann. Pure Appl. Log. 170(7), 825–841 (2019)MathSciNetzbMATHCrossRefGoogle Scholar
 24.Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)zbMATHCrossRefGoogle Scholar
 25.Peuter, D., SofronieStokkermans, V.: On invariant synthesis for parametric systems. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 385–405. Springer, Cham (2019). https://doi.org/10.1007/9783030294366_23CrossRefGoogle Scholar
 26.Pitts, A.M.: On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log. 57(1), 33–52 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
 27.Segerberg, K.: An Essay in Classical Modal Logic. Filosofiska Studier, vol. 13. Uppsala Universitet (1971)Google Scholar
 28.Shavrukov, V.: Subalgebras of diagonalizable algebras of theories containing arithmetic. Dissertationes Mathematicae, CCCXXIII (1993)Google Scholar
 29.SofronieStokkermans, V.: On interpolation and symbol elimination in theory extensions. Log. Methods Comput. Sci. 14(3), 1–41 (2018)MathSciNetzbMATHGoogle Scholar
 30.Tinelli, C., Harandi, M.: A new correctness proof of the NelsonOppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems. ALS, vol. 3, pp. 103–119. Springer, Dordrecht (1996). https://doi.org/10.1007/9789400903494_5zbMATHCrossRefGoogle Scholar
 31.van Gool, S.J., Metcalfe, G., Tsinakis, C.: Uniform interpolation and compact congruences. Ann. Pure Appl. Log. 168(10), 1927–1948 (2017)MathSciNetzbMATHCrossRefGoogle Scholar
 32.Visser, A.: Uniform interpolation and layered bisimulation. In Hájek, P. (ed.) Gödel 1996. Logical Foundations on Mathematics, Computer Science and Physics – Kurt Gödel’s Legacy. Springer, Heidelberg (1996)Google Scholar
 33.Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005). https://doi.org/10.1007/11532231_26CrossRefGoogle Scholar