=Paper=
{{Paper
|id=Vol-2908/short12
|storemode=property
|title=Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality
|pdfUrl=https://ceur-ws.org/Vol-2908/short12.pdf
|volume=Vol-2908
|authors=Elisabeth Henkel,Jochen Hoenicke,Tanja Schindler
|dblpUrl=https://dblp.org/rec/conf/smt/HenkelHS21
}}
==Proof Tree Preserving Sequence Interpolation of Quantified Formulas in the Theory of Equality==
<pdf width="1500px">https://ceur-ws.org/Vol-2908/short12.pdf</pdf>
<pre>
Proof Tree Preserving Sequence Interpolation of
Quantified Formulas in the Theory of Equality
(work in progress)

Elisabeth Henkel, Jochen Hoenicke and Tanja Schindler
Department of Computer Science, University of Freiburg, Germany


                                      Abstract
                                      Interpolation of SMT formulas is difficult, especially in the presence of quantifiers since quantifier
                                      instantiations introduce mixed terms, i.e., terms containing symbols that belong to different partitions of
                                      the input formula. Existing interpolation algorithms for quantified formulas require proof modifications
                                      or syntactical restrictions on the generated proof trees. We present a non-restrictive, proof tree preserving
                                      approach to compute inductive sequences of interpolants for quantified formulas in the theory of equality
                                      with uninterpreted functions using a single proof tree.

                                      Keywords
                                      SMT, interpolation, quantified formulas, sequence interpolants, proof tree preserving interpolation




1. Introduction
We present an interpolation procedure for quantified formulas in the theory of equality with
uninterpreted functions. Interpolants have various applications in model checking, for example,
during abstraction refinement or invariant generation [1, 2, 3, 4]. For the analysis of sequential
programs, sequence interpolants [2] that are computed from infeasible error paths, are of
particular interest. For each point of a program path, a sequence interpolant provides a reason
why an error is unreachable from this point on. Often, the interpolant is general enough to
exclude several paths at once.
   Many verification problems require the ability to reason about quantifiers, which are, among
others, needed in user-added assertions, for the modeling of unsupported theories or memory
modeling [5, 6]. However, the support of interpolation in the presence of quantified formulas
is limited. A major challenge are mixed terms that are introduced in the context of quantifier
instantiations. Most interpolation algorithms are either restricted to quantifier-free input for-
mulas [7, 8, 9, 10, 11, 12, 13], require proof modifications [14], or require syntactical restrictions
on the generated proof trees [15, 16, 17].
   Our method is based on the proof tree preserving interpolation approach [12, 13] which
allows for interpolation of quantifier-free formulas in the presence of mixed literals without the
need for proof modifications or solver restrictions. In particular, sequence or tree interpolants

SMT 2021, 19th International Workshop on Satisfiability Modulo Theories, July 18 - 19, 2021
" henkele@informatik.uni-freiburg.de (E. Henkel); hoenicke@informatik.uni-freiburg.de (J. Hoenicke);
schindle@informatik.uni-freiburg.de (T. Schindler)
                                    © 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
 CEUR
 Workshop
 Proceedings
               http://ceur-ws.org
               ISSN 1613-0073       CEUR Workshop Proceedings (CEUR-WS.org)



                                                                                                        3
can be computed from one single proof of unsatisfiability. We extend this procedure to handle
instantiation-based resolution proofs of quantified formulas similar to [14]. However, we
simplify the presented quantifier introduction step and perform all necessary modifications
only virtually such that the proof tree preserving character is restored.
   The contributions of this paper are a proof tree and satisfiability preserving scheme for the
virtual modification of mixed terms, a scheme to interpolate instantiation clauses generated by
a quantifier solver, and modifications of interpolation rules for theory lemmas and resolvents to
generate valid inductive sequences of interpolants from a single proof tree.

Related Work. Interpolation goes back to Craig [18] who proved that for a valid implication
𝐴 → 𝐵 in first-order logic, there always exists an interpolant (Craig called it “intermediate”),
i.e., a formula 𝐼 that is implied by 𝐴 and implies 𝐵, and that contains only symbols that 𝐴 and
𝐵 share. Since then, several methods for computing interpolants from proofs of unsatisfiability
have been presented both for quantifier-free and quantified problems. We focus our presentation
on some of the most recent and some of the closest related works, and refer to [15, 19] for an
overview of existing work before 2015. Most work on interpolation in the presence of quantified
formulas has been done in the context of automated theorem proving.
   Gleiss et al. [17] present an interpolation method based on splitting the proof of unsatisfiability
into local subproofs. Their method can be applied to arbitrary first-order theories, but requires
local proofs, i.e., proofs where each inference can be assigned to one partition as all occurring
symbols lie in one partition. Each subproof that only uses inferences assigned to 𝐴 is then
summarized in an intermediant. For local proofs, the conjunction of these intermediants is an
interpolant. The method is implemented in the Vampire theorem prover [20].
   Bonacina and Johansson [15] present a method for interpolation in first-order logic with
equality in the context of the superposition calculus which first computes provisional interpolants
and then quantifies over constants that are not shared between 𝐴 and 𝐵. Their method does
not require local proofs, but only yields interpolants if the only non-shared symbols in the
provisional interpolants are constants. The authors also discuss how the method can be used in
the DPLL(Γ + 𝒯 ) calculus [21], but to our knowledge, there does not exist an implementation.
   The method presented by Kovács and Voronkov [16] does not require local proofs either. They
also follow a two-step approach, first computing relational interpolants and then quantifying
over non-shared symbols. In contrast to [15], their method can deal with non-shared function
symbols in the relational interpolants, but is restricted to logic without equality.
   A basis for our work is the interpolation method by Christ and Hoenicke [14] for instantiation-
based proofs in SMT solvers. It relies on proof transformations to obtain a purified proof where
all instances of quantified formulas are local. This is achieved by introducing variables and
auxiliary equations relating the variables to the terms they replace. To obtain an interpolant,
these variables are bound by quantifiers once the terms they replace are resolved from the proof.
   Finally, Christ et al. [12] present a framework that allows for computing quantifier-free
interpolants for quantifier-free problems from a given proof of unsatisfiability without modifying
the proof. In particular, it deals with mixed literals containing non-shared terms from both 𝐴
and 𝐵 by auxiliary variables and more complex interpolation rules. We describe this method in
more detail in Section 3.




                                                  4
2. Notation
We assume the usual notions of first-order logic. A theory 𝒯 is defined by a signature that
contains interpreted and uninterpreted constant, function, and predicate symbols, and by a set
of axioms that settle the meaning for its interpreted symbols. We consider the theory of equality
(with uninterpreted functions), whose axioms state reflexivity, symmetry, and transitivity for
the single interpreted symbol, the equality predicate =, and congruence for each uninterpreted
function symbol.
   As usual, a term is a variable, a constant, or an application of an 𝑛-ary function symbol to 𝑛
terms. An atom is the formula that is always true (⊤), an equality between two terms, or the
application of an 𝑛-ary predicate to 𝑛 terms. A literal is an atom or its negation. A clause is a
disjunction of literals, and a formula is in conjunctive normal form (CNF) if it is a conjunction of
clauses. We assume that formulas are in CNF where each clause can be preceded by universal
quantifiers only. This can be accomplished by Skolemization.
   We usually denote functions by 𝑓, 𝑔, ℎ, terms by 𝑎, 𝑏, 𝑠, 𝑡, variables by 𝑣, 𝑥, 𝑦, 𝑧, literals by ℓ,
clauses by 𝐶, the empty clause by ⊥, and formulas by 𝜑, 𝜓, 𝐴, 𝐵, 𝐼. For two formulas 𝜑 and 𝜓,
we use 𝜑 |= 𝜓 to denote that 𝜓 is a logical consequence of 𝜑 in the theory of equality. Formula
𝜑 is unsatisfiable if and only if 𝜑 |= ⊥. We denote the equivalence of two formulas by 𝜑 ≡ 𝜓. A
formula is said to be ground if it does not contain any variable.
   A substitution maps variables to terms. We denote the result of substituting the terms ¯𝑡 for the
variables 𝑥
          ¯ in a formula 𝜑(𝑥  ¯ ) by 𝜑(𝑡¯). We call a substitution ground if the terms ¯𝑡 are ground.
By 𝜑[ℓ] we denote a formula in negation normal form where the literal ℓ only occurs positively,
and by 𝜑[𝜓] the same formula where all occurrences of ℓ are replaced by the formula 𝜓.


3. Preliminaries
The basis for our interpolation procedure is an instantiation-based resolution proof for the
unsatisfiability of a given formula. We shortly describe the structure of such proofs and how
interpolants can be computed from ground resolution proofs.

Instantiation-Based Resolution Proofs. An instance of a quantified formula ∀𝑥                    ¯ ) is
                                                                                            ¯ .𝜑(𝑥
the result of applying a ground substitution for the variables 𝑥  ¯ to the body 𝜑, i.e., the formula
𝜑(𝑡¯) for ground terms ¯𝑡. Most SMT solvers treat problems containing quantified formulas by
successively adding instances of the quantified formulas to the ground part which is then solved
in the usual way (e.g., with the DPLL(𝒯 )/CDCL algorithm). This approach is mainly suitable to
show unsatisfiability of a formula, but it can also show satisfiability in some restricted fragments.
   A resolution proof for the unsatisfiability of a formula in CNF is a derivation of the empty
clause ⊥ using the rule
                                       𝐶1 ∨ ℓ        𝐶2 ∨ ¬ℓ
                                              𝐶1 ∨ 𝐶2
where 𝐶1 and 𝐶2 are clauses, and ℓ is a literal called the pivot (literal). A resolution proof can
be represented by a tree. For a formula in a theory 𝒯 that contains quantified subformulas,
the tree has three types of leaves: input clauses, theory lemmas, i.e., clauses that are valid in



                                                  5
the theory 𝒯 , and instantiation clauses of the form ¬(∀𝑥     ¯ )) ∨ 𝜑(𝑡¯). Note that we treat the
                                                         ¯ .𝜑(𝑥
quantified formula as a literal which also occurs positively as an input clause. The inner nodes
are clauses obtained by resolution, and the unique root node is the empty clause ⊥.

Interpolation. A Craig interpolant [18] for an unsatisfiable conjunction 𝐴 ∧ 𝐵 is a formula
𝐼 that is implied by 𝐴, contradicts 𝐵, and contains only symbols that occur in both 𝐴 and
𝐵.1 The notion of a Craig interpolant extends to formulas in a theory 𝒯 , in this case, symbols
interpreted by the theory may occur in the interpolant. The notion of binary interpolants can
be generalized to sequences of formulas. Given such a sequence of formulas 𝜑1 , . . . , 𝜑𝑛 that
together are unsatisfiable, a sequence interpolant [2] 𝐼0 , . . . , 𝐼𝑛 has the following properties:

    1. the formulas 𝐼0 and 𝐼𝑛 are ⊤ and ⊥, respectively,

    2. the sequence of interpolants is inductive, i.e., for 𝑖 = 0, . . . , 𝑛, the interpolant 𝐼𝑖 together
       with the formula 𝜑𝑖+1 implies the next interpolant 𝐼𝑖+1 , and

    3. for 𝑖 = 1, . . . , 𝑛, each interpolant 𝐼𝑖 contains only symbols that occur both in some of
       the formulas 𝜑1 , . . . , 𝜑𝑖 and in some of the formulas 𝜑𝑖+1 , . . . 𝜑𝑛 .

We call the formulas 𝜑𝑖 the partitions2 of the interpolation problem. If a symbol occurs in
two partitions 𝜑𝑗 and 𝜑𝑘 , we can assume that it also occurs in all partitions between 𝑗 and
𝑘 without changing the symbol condition of the sequence interpolants. Therefore, we say a
symbol virtually occurs in 𝜑𝑖 if it occurs in some 𝜑𝑗 with 𝑗 ≤ 𝑖 and in some 𝜑𝑘 with 𝑖 ≤ 𝑘.
   Each interpolant 𝐼𝑖 in a sequence interpolant is also a binary interpolant of 𝐴𝑖 :≡ 𝜑1 ∧· · ·∧𝜑𝑖
and 𝐵𝑖 :≡ 𝜑𝑖+1 ∧ · · · ∧ 𝜑𝑛 . Note that not every sequence of binary interpolants obtained by
such partitioning is a sequence interpolant. A literal is mixed if there is no partition 𝜑𝑖 where all
symbols of the literal virtually occur. All literals of the input problem are obviously not mixed,
but mixed literals can be introduced by Nelson-Oppen equality propagation.
   Interpolants can be computed from resolution proofs, e.g., with the interpolation systems by
Pudlák [7] or by McMillan [8]. The general idea is to compute so-called partial interpolants
for every formula proved in the intermediate steps. For resolution proofs such a formula is a
clause 𝐶. The conjunction ¬𝐶 is split and added to the input formulas to obtain a sequence
interpolation problem. First, each term and literal is given one or more colors that correspond to
the partitions where it occurs. A term that occurs in multiple partitions can be given multiple
colors, or a color can be chosen arbitrarily. If a term has multiple colors, we require that the
set of colors forms an interval [𝑖, 𝑗]. We define the projection ¬𝐶 ⇂ 𝜑𝑖 as the conjunction of all
literals in ¬𝐶 that have color 𝑖. In particular, ℓ ⇂ 𝜑𝑖 is ℓ if ℓ has color 𝑖, and ⊤ otherwise. Then
the partial interpolant of 𝐶 is a sequence interpolant of 𝜑1 ∧ ¬𝐶 ⇂ 𝜑1 , . . . , 𝜑𝑛 ∧ ¬𝐶 ⇂ 𝜑𝑛 . The
interpolation systems of Pudlák and McMillan only differ in the way they define the coloring:
for Pudlák a shared literal is colored with all partitions it occurs in, for McMillan a shared literal
is colored with only the last partition it occurs in. Both systems require that each literal has at
     1
       As mentioned in the related work, Craig originally defined an interpolant for a valid implication 𝐴 → 𝐵, i.e.,
as a formula implied by 𝐴 and contradictory to 𝐵. The notion we use is also known as reverse interpolant [22].
     2
       The word partition can be used in English for the sections, or the boundaries, or the whole partitioning. In this
paper we use the word partition for one section of the partitioning.



                                                           6
least one color and that all symbols in the literal occur in the corresponding partition. Mixed
literals require a different interpolation scheme where projections ℓ ⇂ 𝜑𝑖 are defined differently.

Proof Tree Preserving Interpolation. The proof tree preserving interpolation framework
allows for computing binary [12] and sequence or tree interpolants [13] in the presence of mixed
equality literals without modifying a given proof tree. It works with equality interpolating
theories [9, 23].
   A mixed equality literal 𝑎 = 𝑏 or 𝑎 ̸= 𝑏 is a literal where 𝑎 is colored with [𝑗 ′ , 𝑗] and 𝑏 is
colored with [𝑘, 𝑘 ′ ] where these intervals are disjoint. W.l.o.g., we assume that 𝜑𝑗 < 𝜑𝑘 . We
also say that this literal is 𝑗, 𝑘-mixed. The basic idea is to use a fresh auxiliary variable 𝑥 for
each mixed equality literal. When projecting a 𝑗, 𝑘-mixed literal, we split it into two literals
using the auxiliary variable.

   (𝑎 = 𝑏) ⇂ 𝜑𝑗 :≡ (𝑎 = 𝑥)   (𝑎 = 𝑏) ⇂ 𝜑𝑘 :≡ (𝑥 = 𝑏)    (𝑎 = 𝑏) ⇂ 𝜑𝑖 :≡ ⊤ for 𝑖 ̸= 𝑗, 𝑘
   (𝑎 ̸= 𝑏) ⇂ 𝜑𝑗 :≡ EQ(𝑥, 𝑎) (𝑎 =                          ̸ 𝑏) ⇂ 𝜑𝑖 :≡ ⊤ for 𝑖 ̸= 𝑗, 𝑘
                                ̸ 𝑏) ⇂ 𝜑𝑘 :≡ ¬ EQ(𝑥, 𝑏) (𝑎 =

Here, EQ is an uninterpreted predicate that forces the interpolant to have a certain shape. The
interpolation procedure treats EQ and 𝑥 as shared symbols, which may occur in the interpolant.
Note that ℓ ⇂ 𝜑𝑗 ∧ ℓ ⇂ 𝜑𝑘 is equisatisfiable to ℓ and has the same models for the symbols in ℓ.
   Again, we define the partial interpolants of a clause 𝐶 as the sequence interpolant for the
sequence 𝜑1 ∧ ¬𝐶 ⇂ 𝜑1 , . . . , 𝜑𝑛 ∧ ¬𝐶 ⇂ 𝜑𝑛 . If the negation ¬𝐶 of a clause contains a mixed
equality 𝑎 = 𝑏, the partial interpolants 𝐼𝑖 for 𝐶 with 𝑗 ≤ 𝑖 < 𝑘 may contain the auxiliary
variable 𝑥. If ¬𝐶 contains 𝑎 ̸= 𝑏, we require that the variable 𝑥 in the interpolant 𝐼𝑖 only occurs
in atoms of the form EQ(𝑥, 𝑠𝑙 ) which must occur positively in 𝐼𝑖 . This is not really a restriction
as interpolants naturally have this shape. The 𝑠𝑙 are shared terms, which are closely related to
equality-interpolating terms in the sense of [9].
   As mentioned earlier, an interpolant is computed by annotating each clause 𝐶 in the proof tree,
starting with the leaves, by a partial interpolant 𝐼0 , . . . , 𝐼𝑛 . We denote this by 𝐶 : 𝐼1 , . . . , 𝐼𝑛−1
(we omit 𝐼0 ≡ ⊤ and 𝐼𝑛 ≡ ⊥). Resolution combines the partial interpolants of the involved
clauses. To resolve on a mixed literal 𝑎 = 𝑏, we combine the partial interpolants of the input
clauses using the following function that replaces all occurrences of EQ(𝑥, 𝑠𝑙 ) in 𝐼 by a copy
of 𝐼 ′ where all occurrences of 𝑥 are replaced by 𝑠𝑙 .

            ruleEq(𝑎 = 𝑏, 𝐼[EQ(𝑥, 𝑠1 )]...[EQ(𝑥, 𝑠𝑚 )], 𝐼 ′ (𝑥)) :≡ 𝐼[𝐼 ′ (𝑠1 )]...[𝐼 ′ (𝑠𝑚 )]

The following rule is used to compute the partial interpolants for the resolvent of a resolution
rule from the partial interpolants of the antecedents.

                   𝐶1 ∨ ℓ : 𝐼1 , . . . , 𝐼𝑛−1    𝐶2 ∨ ¬ℓ : 𝐼1′ , . . . , 𝐼𝑛−1
                                                                          ′

                                  𝐶1 ∨ 𝐶2 : 𝐼1′′ , . . . , 𝐼𝑛−1
                                                            ′′
                   ⎧
                     𝐼𝑖 ∨ 𝐼𝑖′                 if ℓ has only colors 𝑗 ≤ 𝑖,
                                                                                              (resolution)
                   ⎪
                   ⎪
                   ⎪
                                              if ℓ has only colors 𝑗 > 𝑖,
                   ⎪
                   ⎨𝐼 ∧ 𝐼
                      𝑖    𝑖
      with 𝐼𝑖′′ :≡
                   ⎪ruleEq(ℓ, 𝐼𝑖 , 𝐼𝑖 )
                   ⎪
                   ⎪
                                         ′    if ℓ is 𝑗, 𝑘-mixed, 𝑗 ≤ 𝑖 < 𝑘,
                   ⎩(𝐼 ∨ ℓ) ∧ (𝐼 ′ ∨ ¬ℓ) if ℓ has colors [𝑗, 𝑘] with 𝑗 ≤ 𝑖 < 𝑘.
                   ⎪
                        𝑖            𝑖




                                                     7
Example 1 (Mixed Literals). Consider the following two (tautological) clauses
             𝐶 :≡ 𝑎 = 𝑏 ∨ 𝑎 ̸= 𝑡 ∨ 𝑡 ̸= 𝑏      𝐶 ′ :≡ 𝑎 ̸= 𝑏 ∨ 𝑠 ̸= 𝑓 (𝑎) ∨ 𝑠 = 𝑓 (𝑏),
where 𝑎 is 𝜑1 -local, 𝑏 is 𝜑2 -local, and the remaining symbols are shared. A partial interpolant
of 𝐶 is the formula EQ(𝑥, 𝑡), since it is an interpolant of
            ¬𝐶 ⇂ 𝜑1 ≡ EQ(𝑥, 𝑎) ∧ 𝑎 = 𝑡        and ¬𝐶 ⇂ 𝜑2 ≡ ¬ EQ(𝑥, 𝑏) ∧ 𝑏 = 𝑡 .
This interpolant can be obtained by using well-known interpolation techniques for the theory
of equality. Note that EQ(𝑥, 𝑡) captures the equality-interpolating term 𝑡 of 𝑎 = 𝑏 in the sense
of [9]. For the second clause 𝐶 ′ , the formula 𝑠 = 𝑓 (𝑥) is a partial interpolant, i.e., it is an
interpolant of
            ¬𝐶 ′ ⇂ 𝜑1 ≡ 𝑎 = 𝑥 ∧ 𝑠 = 𝑓 (𝑎) and ¬𝐶 ′ ⇂ 𝜑2 ≡ 𝑥 = 𝑏 ∧ 𝑠 ̸= 𝑓 (𝑏) .
The interpolant for the resolvent of 𝐶 and 𝐶 ′ can now be obtained using the resolution rule:
       𝑎 = 𝑏 ∨ 𝑎 ̸= 𝑡 ∨ 𝑡 ̸= 𝑏 : EQ(𝑥, 𝑡)        𝑎 ̸= 𝑏 ∨ 𝑠 ̸= 𝑓 (𝑎) ∨ 𝑠 = 𝑓 (𝑏) : 𝑠 = 𝑓 (𝑥)
                       𝑎 ̸= 𝑡 ∨ 𝑠 ̸= 𝑓 (𝑎) ∨ 𝑡 ̸= 𝑏 ∨ 𝑠 = 𝑓 (𝑏) : 𝑠 = 𝑓 (𝑡)
The interested reader is invited to check that the annotated partial interpolant is correct.


4. Mixed Terms
One obstacle to use proof tree preserving interpolation in the presence of quantifiers are mixed
terms. To illustrate the problem, let us consider the following example.
Example 2 (Running Example). Take the sequence of formulas 𝜑1 , 𝜑2 , 𝜑3 with
                𝜑1 : ∀𝑥.𝑔(ℎ(𝑥)) = 𝑥 𝜑2 : ∀𝑦.𝑓 (𝑔(𝑦)) ̸= 𝑏 𝜑3 : ∀𝑧.𝑓 (𝑧) = 𝑧.
The conjunction of the three formulas is unsatisfiable, which can be seen as follows. Instantiating
𝜑1 with 𝑏 gives 𝑔(ℎ(𝑏)) = 𝑏. Instantiating 𝜑2 with ℎ(𝑏) gives 𝑓 (𝑔(ℎ(𝑏))) ̸= 𝑏. Substituting
𝑔(ℎ(𝑏)) using the first equality yields 𝑓 (𝑏) ̸= 𝑏, which is clearly a contradiction to 𝜑3 .
   A mixed term is a term that uses symbols from at least two different partitions. In the example
above, a mixed term is ℎ(𝑏), because ℎ only occurs in 𝜑1 and 𝑏 only occurs in 𝜑2 . Mixed terms
may be generated during the instantiation process of quantified formulas. They can thus appear
in a resolution proof within instantiation clauses and theory lemmas but not in input clauses. A
resolution node may contain a mixed term if it was already contained in one of its antecedents.
Interpolation algorithms based on resolution proofs usually rely upon non-mixed terms. We do
not want to restrict the instantiation procedure to local terms as this would negatively effect
the performance of the solver. Transforming the proofs into localized proofs in the context of
sequence interpolation can break the inductivity property if not done in a consistent manner.
So it would require to either localize the proof for all partitions at once or to compute the
interpolants by repeated binary interpolation, which requires a new proof for each interpolant.
   We propose a method to handle mixed terms, simply by coloring them with some input
partition. This partition does not contain all symbols occurring in the term. Thus, we replace
subterms of the wrong color by fresh variables to purify the term. Each variable is defined by
adding an auxiliary equation to all partitions where the subterm’s outer function symbol occurs.



                                                8
4.1. Purification of Mixed Literals
We proceed by first assigning a color to each term, and purify mixed terms afterwards. As a
symbol may appear in several partitions, we can assign one or multiple of these partitions as its
color. However, this decision may affect the number of quantifiers within the final interpolant.
We use the following coloring scheme to obtain as few quantifiers as possible. To color a term,
we start by coloring its subterms from bottom up. The color of a constant symbol corresponds to
the partitions it occurs in. For a function application 𝑓 (𝑡1 , . . . , 𝑡𝑛 ), we compute the intersection
of the partitions where 𝑓 occurs and the colors of the terms 𝑡1 , . . . , 𝑡𝑛 . If the intersection is
non-empty, it is used to color the term. Otherwise, if it is empty, meaning that the term contains
symbols for which there is no common partition. We color the term by all partitions in which
the function symbol 𝑓 occurs. The whole literal is then colored as if the top-level terms occurred
in the partitions corresponding to the terms’ colors.
   If the literal ℓ colored with partition 𝑖 contains a mixed term, it contains some constant 𝑐
or function application 𝑓 (𝑡1 , . . . , 𝑡𝑛 ) where 𝑐 or 𝑓 does not occur in the partition 𝑖. In the
projection ℓ ⇂ 𝜑𝑖 , these constants and function applications are replaced by fresh variables
𝑣𝑓 (𝑡1 ,...,𝑡𝑛 ) . Each fresh variable is set equal to the term it stands for by an auxiliary equation of the
form 𝑣𝑓 (𝑡1 ,...,𝑡𝑛 ) = 𝑓 (𝑣𝑡1 , . . . , 𝑣𝑡𝑛 ). The arguments of the function application are also replaced
by fresh variables and the corresponding auxiliary equations are added to their corresponding
partitions, i.e., the term is flattened.
Example 3 (Purification). Take the sequence of formulas 𝜑1 , 𝜑2 , 𝜑3 from the running example
(Example 2). Consider the literal ℓ ≡ 𝑔(ℎ(𝑏)) = 𝑏 that stems from instantiating 𝜑1 . The subterm
𝑏 occurs only in partition 2. The term ℎ(𝑏) is mixed since ℎ only occurs in partition 1. We assign
it partition 1. The term 𝑔(ℎ(𝑏)) is now also assigned partition 1 as it is the intersection where 𝑔
occurs (1, 2) and what its argument ℎ(𝑏) was assigned. The whole literal is treated as mixed
equality, since the left-hand side 𝑔(ℎ(𝑏)) of ℓ is colored 1 and the right-hand side 𝑏 is colored 2.
   When computing the projection of the mixed equality ℓ ⇂ 𝜑𝑖 , we split ℓ first into 𝑔(ℎ(𝑏)) = 𝑥
and 𝑥 = 𝑏, as we explained in Section 3. In the projection, we further replace the subterm 𝑏 on
the left-hand side (that does not match partition 1) with a fresh variable. The auxiliary equation
is added to partition 2, since this is the partition where 𝑏 occurs.

    ℓ ≡ 𝑔(ℎ(𝑏)) = 𝑏 :       ℓ ⇂ 𝜑1 ≡ 𝑔(ℎ(𝑣𝑏 )) = 𝑥,         ℓ ⇂ 𝜑2 ≡ 𝑥 = 𝑏 ∧ 𝑣𝑏 = 𝑏,      ℓ ⇂ 𝜑3 ≡ ⊤

Consider the literal ℓ ≡ 𝑓 (𝑔(ℎ(𝑏))) = 𝑏 that stems from instantiating 𝜑2 . As before, the term
𝑔(ℎ(𝑏)) is assigned partition 1. The term 𝑓 (𝑔(ℎ(𝑏))) is mixed as 𝑓 is only in partition 2, 3. So
the whole term gets assigned partitions 2, 3. Since the right-hand side 𝑏 of the equality appears
only in partition 2, the whole literal is assigned partition 2.
   When computing the projection, we replace all subterms not occurring in partition 2 with
fresh variables, as well as their subterms. The auxiliary equations are added to the partitions
where the corresponding function symbol appears.

ℓ ≡ 𝑓 (𝑔(ℎ(𝑏))) = 𝑏 :      ℓ ⇂ 𝜑1 ≡ 𝑣ℎ = ℎ(𝑣𝑏 ),         ℓ ⇂ 𝜑2 ≡ 𝑓 (𝑔(𝑣ℎ )) = 𝑏 ∧ 𝑣𝑏 = 𝑏,     ℓ ⇂ 𝜑3 ≡ ⊤

Note that if ℎ occurred in multiple partitions, the auxiliary equation 𝑣ℎ = ℎ(𝑣𝑏 ) would be added
to all projections where ℎ occurs in the partition.



                                                     9
4.2. Quantifier Introduction
As mentioned in Section 3, our algorithm computes for each clause 𝐶 in the resolution proof a
partial interpolant of 𝜑1 ∧¬𝐶 ⇂ 𝜑1 , . . . , 𝜑𝑛 ∧¬𝐶 ⇂ 𝜑𝑛 . Interpolation of leaf clauses is performed
based on the color of literals, i.e., the interpolants are computed as if the literal occurred in the
partition corresponding to its color. This may introduce symbols from the wrong partition in the
interpolant, i.e., the resulting interpolant may violate the symbol condition. The algorithm then
replaces all terms containing symbols that are not allowed in the interpolant by their auxiliary
variable. In many cases, these auxiliary variables are allowed to occur in the partial interpolant,
since they satisfy the symbol condition with respect to the corresponding interpolation problem
𝜑1 ∧ ¬𝐶 ⇂ 𝜑1 , . . . , 𝜑𝑛 ∧ ¬𝐶 ⇂ 𝜑𝑛 .
   We say that a variable 𝑣 is supported by a clause 𝐶 if the term that it replaced occurs within
a mixed term in 𝐶, that is, if the auxiliary equation defining 𝑣 is part of one of the projections
¬𝐶 ⇂ 𝜑𝑖 . Note that a variable may be unsupported even if the corresponding subterm occurs
in the clause, e.g., 𝑣𝑏 is not supported by 𝑓 (𝑏) ̸= 𝑏, because the literal contains no mixed term
and thus there is no auxiliary equation for 𝑣𝑏 . A variable may only appear unbound in the
partial interpolant of a clause 𝐶 if it is supported by 𝐶. Thus, in a post-processing step, we bind
variables that are not supported by the current clause but still occur in a partial interpolant. An
existential quantifier is introduced around the interpolant 𝐼𝑖 for each unsupported variable 𝑣𝑓
where the head function symbol 𝑓 appears in 𝐴𝑖 . Similarly, a universal quantifier is introduced
for 𝑣𝑓 if 𝑓 appears in 𝐵𝑖 . If multiple variables become unsupported at the same time, we need
to be careful to add the quantifiers in the right order. If one of the variables corresponds to
a subterm of the other, then the variable for the outer term is defined using the variable of
the subterm. Hence its quantifier needs to appear after the quantifier for the variable of the
outer term. Since we add quantifiers from inside to outside, we need to add the quantifiers in
inverse dependency order, i.e., the quantifier for the variable corresponding to the outermost
term needs to be added first.


5. Interpolation for Quantified Formulas
In this section, we show how to compute partial sequence interpolants for the different clause
types involved in a proof of unsatisfiability for quantified input formulas. The overall algorithm
follows a simple common theme: first compute the interpolants using only the colors we
assigned to literals and ignore the symbol condition. Then introduce the fresh variable 𝑣𝑡 for
every term 𝑡 that violates the symbol condition. Finally, introduce quantifiers for each variable
𝑣𝑡 that is unsupported by the current clause, as outlined in Section 4.2. In the following, we
concretize this for the different kind of clauses in the resolution proof.

Input Clauses. Input clauses cannot contain mixed terms. The interpolant 𝐼𝑖 of an input
clause 𝐶 is either ¬(¬𝐶 ∖ 𝐴𝑖 ) if the clause 𝐶 is part of 𝐴𝑖 , or ¬𝐶 ∖ 𝐵𝑖 if 𝐶 is part of 𝐵𝑖 . Here
¬𝐶 ∖ 𝐴𝑖 removes all literals from 𝐶 that do not have any color from 𝐴𝑖 . For Pudlák’s algorithm
where each literal is colored with all partitions it occurs in, all literals are removed and the
interpolants are always either ⊤ or ⊥.




                                                 10
Instantiation Clauses. We say that an instantiation clause originates from the partition
in which its quantified formula occurs in. We extend the definition of ¬𝐶 ∖ 𝐴𝑖 to handle a
𝑗, 𝑘-mixed equality 𝑎 = 𝑏 as follows: if both 𝑎, 𝑏 are in 𝐴𝑖 , then (ℓ ∖ 𝐴𝑖 ) ≡ ⊤, if both are
in 𝐵𝑖 , then (ℓ ∖ 𝐴𝑖 ) ≡ ℓ, and if 𝑎 is in 𝐴𝑖 and 𝑏 in 𝐵𝑖 , then (𝑎 = 𝑏 ∖ 𝐴𝑖 ) ≡ 𝑥 = 𝑏 and
(𝑎 ̸= 𝑏 ∖ 𝐴𝑖 ) ≡ ¬ EQ(𝑥, 𝑏). Analogously, we define ¬𝐶 ∖ 𝐵𝑖 . The partial sequence interpolant
𝐼𝑖 is then computed in three steps.
   1. Set 𝐼𝑖 to ¬(¬𝐶 ∖ 𝐴𝑖 ) if 𝐶 originates from 𝐴𝑖 , and to ¬𝐶 ∖ 𝐵𝑖 , otherwise.
   2. Replace every subterm 𝑡 in 𝐼𝑖 that must not occur in 𝐼𝑖 according to the symbol condition
      by its corresponding fresh variable 𝑣𝑡 .
   3. Introduce quantifiers for each variable that is not supported by 𝐶.

Theory Lemmas.            Our proof tree can contain theory lemmas for transitivity and congruence.
               𝑡1 ̸= 𝑡2 ∨ · · · ∨ 𝑡𝑛−1 ̸= 𝑡𝑛 ∨ 𝑡1 = 𝑡𝑛                                         (transitivity)
               𝑡1 ̸= 𝑡′1 ∨ · · · ∨ 𝑡𝑛 ̸= 𝑡′𝑛 ∨ 𝑓 (𝑡1 , . . . , 𝑡𝑛 ) = 𝑓 (𝑡′1 , . . . , 𝑡′𝑛 )   (congruence)
Transitivity lemmas are interpolated by summarizing equality chains involving 𝐴𝑖 -colored
literals in the negation of the lemma. If the single equality of the transitivity lemma is mixed, the
chain EQ(𝑥, 𝑎1 ) ∧ 𝑎1 = · · · = 𝑎𝑛 is summarized by EQ(𝑥, 𝑎𝑛 ). As the ends of the 𝐴𝑖 -colored
chains are also 𝐵𝑖 -colored (the boundary terms appear in 𝐵𝑖 -colored literals), this satisfies the
symbol condition except when a mixed term contains a subterm from a different partition. To
fix the interpolant, all subterms 𝑡 from the wrong partition are replaced by their corresponding
variable 𝑣𝑡 . Our construction guarantees that these variables are supported by 𝐶.
   For congruence lemmas, the interpolant depends on the color of the equality 𝑓 (𝑡1 , . . . , 𝑡𝑛 ) =
𝑓 (𝑡′1 , . . . , 𝑡′𝑛 ). If it is colored with a partition from 𝐴𝑖 , the interpolant is ¬(¬𝐶 ∖ 𝐴𝑖 ) and if it is
colored with a partition from 𝐵𝑖 , the interpolant is ¬𝐶 ∖ 𝐵𝑖 . If the equality is a mixed equality
where 𝑓 (𝑡1 , . . . , 𝑡𝑛 ) is from 𝐴𝑖 , then 𝑓 is shared and the interpolant is EQ(𝑥, 𝑓 (𝑥1 , . . . , 𝑥𝑛 ))
where 𝑥 is the variable for the projection of the mixed equality, and for 𝑗 = 1, . . . , 𝑛 the term 𝑥𝑗
is the auxiliary variable of 𝑡𝑗 = 𝑡′𝑗 , if that equality is mixed, or 𝑡𝑗 if the equality is colored with
𝐵𝑖 , or 𝑡′𝑗 if it is colored with 𝐴𝑖 . Again, the subterms 𝑡 from the wrong partition are replaced by
their corresponding variable 𝑣𝑡 , which is supported by 𝐶.

Resolution Clauses. The partial interpolant for a resolution node is computed by the rule
(resolution) in Section 3. Since the resolution rule removes a literal from both antecedent clauses,
the resolvent may no longer support all variables occurring in the interpolant. So in the last
step, we add quantifiers for all unsupported variables as outlined in Section 4.2.
Example 4. We illustrate the algorithm on our running example (Example 2).
                   𝜑1 : ∀𝑥.𝑔(ℎ(𝑥)) = 𝑥 𝜑2 : ∀𝑦.𝑓 (𝑔(𝑦)) ̸= 𝑏 𝜑3 : ∀𝑧.𝑓 (𝑧) = 𝑧
The symbol 𝑓 occurs in partitions 2–3, 𝑔 in 1–2, ℎ in 1, 𝑏 in 2. Our goal is to compute sequence
interpolants 𝐼1 , 𝐼2 where 𝜑1 implies 𝐼1 , and 𝐼1 and 𝜑2 imply 𝐼2 , and 𝐼2 and 𝜑3 imply ⊥. Also 𝐼1
may only contain the symbol 𝑔 and 𝐼2 only the symbol 𝑓 .



                                                             11
   Figure 1 gives an instantiation-based resolution proof for the unsatisfiability of 𝜑1 ∧ 𝜑2 ∧ 𝜑3 .
Each clause 𝐶 in the proof tree is annotated with its partial interpolant 𝐼1 , 𝐼2 . In the following,
we explain step by step how these interpolants were computed. First, we color the literals
occurring in the proof. The literals 𝑔(ℎ(𝑏)) = 𝑏 and 𝑓 (𝑔(ℎ(𝑏)) = 𝑏 were already explained in
Section 4.1. The literal 𝑓 (𝑔(ℎ(𝑏))) = 𝑓 (𝑏) is colored the same way as 𝑓 (𝑔(ℎ(𝑏))) = 𝑏. Finally,
the literal 𝑓 (𝑏) = 𝑏 is not mixed and is colored with 2. To summarize, the projection of these
literals to the partitions 1–3 is as follows.
                      ℓ            ℓ ⇂ 𝜑1               ℓ ⇂ 𝜑2          ℓ ⇂ 𝜑3
                𝑔(ℎ(𝑏)) = 𝑏     𝑔(ℎ(𝑣𝑏 )) = 𝑥     𝑥 = 𝑏 ∧ 𝑣𝑏 = 𝑏          ⊤
            𝑓 (𝑔(ℎ(𝑏))) = 𝑓 (𝑏) 𝑣ℎ = ℎ(𝑣𝑏 ) 𝑓 (𝑔(𝑣ℎ )) = 𝑓 (𝑏) ∧ 𝑣𝑏 = 𝑏   ⊤
              𝑓 (𝑔(ℎ(𝑏))) = 𝑏    𝑣ℎ = ℎ(𝑣𝑏 )  𝑓 (𝑔(𝑣ℎ )) = 𝑏 ∧ 𝑣𝑏 = 𝑏     ⊤
                  𝑓 (𝑏) = 𝑏          ⊤                𝑓 (𝑏) = 𝑏           ⊤
The first input clause on the top left of the proof tree is from 𝜑1 , i.e., it is in 𝐴1 and 𝐴2 . By the
rule for input clauses its interpolants are ⊥, ⊥. The projections of the negated instantiation
clause Inst on the top right are
¬Inst ⇂ 𝜑1 ≡ (𝜑1 ∧EQ(𝑥, 𝑔(ℎ(𝑣𝑏 )))) ¬Inst ⇂ 𝜑2 ≡ (¬ EQ(𝑥, 𝑏)∧𝑣𝑏 = 𝑏)                 ¬Inst ⇂ 𝜑3 ≡ ⊤.
For 𝐼1 , the quantified formula is in 𝐴1 , and the interpolant is first set to ¬(¬𝐶 ∖ 𝐴1 ). Since
𝑔(ℎ(𝑏)) = 𝑏 is 1, 2-mixed, (𝑔(ℎ(𝑏)) ̸= 𝑏 ∖ 𝐴1 ) is ¬ EQ(𝑥, 𝑏) and 𝐼1 is set to EQ(𝑥, 𝑏). In the
final step, the forbidden symbol 𝑏 is replaced by its shared variable 𝑣𝑏 yielding EQ(𝑥, 𝑣𝑏 ). The
variable 𝑣𝑏 is supported by the clause and therefore not quantified. The interpolant 𝐼2 is just ⊥
as it contains only literals with colors 1–2. Resolving the first two clauses builds the disjunction
of the corresponding interpolants, because the literal is colored with partition 1.
   The equality in the congruence lemma, in the second row in Figure 1, is colored with partition 2.
Therefore, interpolant 𝐼1 is first set to ¬𝐶 ∖ 𝐵1 , which is 𝑔(ℎ(𝑏)) = 𝑥. As the function symbol
ℎ may not occur in the interpolant, the term ℎ(𝑏) is replaced by its auxiliary variable 𝑣ℎ . The
interpolant 𝐼2 is set to ⊥ since the lemma involves no literal colored with partition 2. The
result is 𝑔(𝑣ℎ ) = 𝑥, ⊥, which is indeed a sequence interpolant of 𝑣ℎ = ℎ(𝑣𝑏 ) ∧ 𝑔(ℎ(𝑣𝑏 )) = 𝑥,
𝑓 (𝑔(𝑣ℎ )) ̸= 𝑓 (𝑏) ∧ 𝑥 = 𝑏 ∧ 𝑣𝑏 = 𝑏, ⊤. The next resolution step involves a 1, 2-mixed literal.
Therefore, we use the third case (ruleEq) of rule (resolution). The first interpolants of the
antecedents are combined by replacing EQ(𝑥, 𝑣𝑏 ) with 𝑔(𝑣ℎ ) = 𝑣𝑏 , yielding 𝑔(𝑣ℎ ) = 𝑣𝑏 . All
literals in the transitivity lemma (third row) are colored with partition 2. Therefore the resulting
interpolants are ⊤, ⊥. The resolution step combines the interpolants with conjunction or
disjunction, respectively, as the literal is colored with partition 2.
   The second instantiation clause is completely colored with partition 2 as is the corresponding
input clause. The interpolants are just ⊤, ⊥ and resolving them with the other branch does not
change the previous interpolants. However, since the literal 𝑓 (𝑔(ℎ(𝑏))) ̸= 𝑏 gets removed in the
resolution step, 𝑣ℎ and 𝑣𝑏 are no longer supported. Therefore, quantifiers are introduced: the
inner existential quantifier for the 1-colored outermost term 𝑣ℎ = ℎ(𝑣𝑏 ) and the outer universal
quantifier for the 2-colored inner term 𝑣𝑏 = 𝑏. Note that although the clause still contains 𝑏 in
the literal 𝑓 (𝑏) ̸= 𝑏, this literal is not mixed and therefore does not support 𝑣𝑏 .
   The last instantiation clause is originating from 𝜑3 , hence 𝐼1 is set to ¬𝐶 ∖ 𝐵1 (which is ⊤)
and 𝐼2 is set to ¬𝐶 ∖ 𝐵2 . Since 𝑓 (𝑏) ̸= 𝑏 is colored with partition 2, the second interpolant is



                                                  12
  ∀𝑥.𝑔(ℎ(𝑥)) = 𝑥 ⊥, ⊥         ¬(∀𝑥.𝑔(ℎ(𝑥)) = 𝑥), 𝑔(ℎ(𝑏)) = 𝑏 EQ(𝑥, 𝑣𝑏 ), ⊥

    𝑔(ℎ(𝑏)) = 𝑏 EQ(𝑥, 𝑣𝑏 ), ⊥        𝑔(ℎ(𝑏)) ̸= 𝑏, 𝑓 (𝑔(ℎ(𝑏))) = 𝑓 (𝑏) 𝑔(𝑣ℎ ) = 𝑥, ⊥

 𝑓 (𝑔(ℎ(𝑏))) = 𝑓 (𝑏) 𝑔(𝑣ℎ ) = 𝑣𝑏 , ⊥      𝑓 (𝑔(ℎ(𝑏))) ̸= 𝑓 (𝑏), 𝑓 (𝑏) ̸= 𝑏, 𝑓 (𝑔(ℎ(𝑏))) = 𝑏 ⊤, ⊥

 𝑓 (𝑏) ̸= 𝑏, 𝑓 (𝑔(ℎ(𝑏))) = 𝑏 𝑔(𝑣ℎ ) = 𝑣𝑏 , ⊥

                           ∀𝑦.𝑓 (𝑔(𝑦)) ̸= 𝑏 ⊤, ⊥           ¬(∀𝑦.𝑓 (𝑔(𝑦)) ̸= 𝑏), 𝑓 (𝑔(ℎ(𝑏))) ̸= 𝑏 ⊤, ⊥

                                  𝑓 (𝑔(ℎ(𝑏))) ̸= 𝑏 ⊤, ⊥

               𝑓 (𝑏) ̸= 𝑏 ∀𝑣𝑏 .∃𝑣ℎ .𝑔(𝑣ℎ ) = 𝑣𝑏 , ⊥
        Input Clause           ∀𝑧.𝑓 (𝑧) = 𝑧 ⊤, ⊤           ¬(∀𝑧.𝑓 (𝑧) = 𝑧), 𝑓 (𝑏) = 𝑏 ⊤, ∃𝑣𝑏 .𝑓 (𝑣𝑏 ) ̸= 𝑣𝑏
    Instantiation Clause
                                          𝑓 (𝑏) = 𝑏 ⊤, ∃𝑣𝑏 .𝑓 (𝑣𝑏 ) ̸= 𝑣𝑏
       Theory Lemma
         Resolvent                     ⊥ ∀𝑣𝑏 .∃𝑣ℎ .𝑔(𝑣ℎ ) = 𝑣𝑏 , ∃𝑣𝑏 .𝑓 (𝑣𝑏 ) ̸= 𝑣𝑏

Figure 1: Refutation by resolution for Example 4 annotated by partial sequence interpolants.


𝑓 (𝑏) ̸= 𝑏. In the next step, 𝑏 is replaced by its auxiliary variable 𝑣𝑏 and since this is not supported
by the clause, an existential quantifier must be introduced. So the partial sequence interpolant is
⊤, ∃𝑣𝑏 .𝑓 (𝑣𝑏 ) ̸= 𝑣𝑏 . This is indeed a valid interpolant for the sequence ⊤, 𝑓 (𝑏) ̸= 𝑏, ∀𝑧.𝑓 (𝑧) = 𝑧.
   In the last two resolution steps, the interpolants are combined with conjunction or disjunction.
Since for each resolution step one of the interpolants is ⊤ or ⊥, the other interpolant is not
changed. The final sequence interpolant, i.e., ∀𝑣𝑏 ∃𝑣ℎ .𝑔(𝑣ℎ ) = 𝑣𝑏 , ∃𝑣𝑏 .𝑓 (𝑣𝑏 ) ̸= 𝑣𝑏 , can be found
in the annotation of the empty clause.


6. Conclusion and Future Work
We presented an algorithm to obtain inductive sequences of interpolants from instantiation-
based refutation proofs of quantified formulas in the theory of equality. In contrast to most
existing algorithms that allow for interpolation of quantified formulas, our approach works
on non-local proofs. It neither requires to restrict the inference done by the SMT solver, nor
does it require transformations of the proof tree. Mixed terms occurring in a proof tree due
to quantifier instantiations are directly treated using virtual purification. To obtain (partial)
interpolants satisfying the symbol condition, local terms are replaced by auxiliary variables
that are eventually bound by quantifiers.
   Our algorithm computes sequence interpolants from a single proof of unsatisfiability instead
of repeatedly performing binary interpolation on several proof trees. Implementation of the
algorithm in SMTInterpol [24] is ongoing work. We plan to extend our algorithm to tree
interpolants as well as to other theories including linear arithmetic.




                                                      13
Acknowledgments
This work was partially supported by the German Research Council (DFG) under HO 5606/1-2.


References
 [1] T. A. Henzinger, R. Jhala, R. Majumdar, K. L. McMillan, Abstractions from proofs, in: N. D.
     Jones, X. Leroy (Eds.), Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on
     Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, ACM,
     2004, pp. 232–244. URL: https://doi.org/10.1145/964001.964021. doi:10.1145/964001.
     964021.
 [2] K. L. McMillan, Lazy abstraction with interpolants, in: T. Ball, R. B. Jones (Eds.), Computer
     Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August
     17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, Springer, 2006,
     pp. 123–136. URL: https://doi.org/10.1007/11817963_14. doi:10.1007/11817963\_14.
 [3] K. L. McMillan, Quantified invariant generation using an interpolating saturation prover,
     in: C. R. Ramakrishnan, J. Rehof (Eds.), Tools and Algorithms for the Construction and
     Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the
     Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest,
     Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer
     Science, Springer, 2008, pp. 413–427. URL: https://doi.org/10.1007/978-3-540-78800-3_31.
     doi:10.1007/978-3-540-78800-3\_31.
 [4] M. Heizmann, J. Hoenicke, A. Podelski, Nested interpolants, in: POPL, ACM, 2010, pp.
     471–482.
 [5] M. N. Seghir, A. Podelski, T. Wies, Abstraction refinement for quantified array assertions,
     in: J. Palsberg, Z. Su (Eds.), Static Analysis, 16th International Symposium, SAS 2009, Los
     Angeles, CA, USA, August 9-11, 2009. Proceedings, volume 5673 of Lecture Notes in Com-
     puter Science, Springer, 2009, pp. 3–18. URL: https://doi.org/10.1007/978-3-642-03237-0_3.
     doi:10.1007/978-3-642-03237-0\_3.
 [6] R. Blanc, A. Gupta, L. Kovács, B. Kragl, Tree interpolation in Vampire, in: K. L.
     McMillan, A. Middeldorp, A. Voronkov (Eds.), Logic for Programming, Artificial Intel-
     ligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South
     Africa, December 14-19, 2013. Proceedings, volume 8312 of Lecture Notes in Computer
     Science, Springer, 2013, pp. 173–181. URL: https://doi.org/10.1007/978-3-642-45221-5_13.
     doi:10.1007/978-3-642-45221-5\_13.
 [7] P. Pudlák, Lower bounds for resolution and cutting plane proofs and monotone
     computations, J. Symb. Log. 62 (1997) 981–998. URL: https://doi.org/10.2307/2275583.
     doi:10.2307/2275583.
 [8] K. L. McMillan, An interpolating theorem prover, in: K. Jensen, A. Podelski (Eds.),
     Tools and Algorithms for the Construction and Analysis of Systems, 10th International
     Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and
     Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings,




                                               14
     volume 2988 of Lecture Notes in Computer Science, Springer, 2004, pp. 16–30. URL: https:
     //doi.org/10.1007/978-3-540-24730-2_2. doi:10.1007/978-3-540-24730-2\_2.
 [9] G. Yorsh, M. Musuvathi, A combination method for generating interpolants, in: R. Nieuwen-
     huis (Ed.), Automated Deduction - CADE-20, 20th International Conference on Automated
     Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, volume 3632 of Lecture Notes in
     Computer Science, Springer, 2005, pp. 353–368. URL: https://doi.org/10.1007/11532231_26.
     doi:10.1007/11532231\_26.
[10] A. Cimatti, A. Griggio, R. Sebastiani, Efficient interpolant generation in satisfiability modulo
     theories, in: C. R. Ramakrishnan, J. Rehof (Eds.), Tools and Algorithms for the Construction
     and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the
     Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest,
     Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer
     Science, Springer, 2008, pp. 397–412. URL: https://doi.org/10.1007/978-3-540-78800-3_30.
     doi:10.1007/978-3-540-78800-3\_30.
[11] A. Fuchs, A. Goel, J. Grundy, S. Krstic, C. Tinelli, Ground interpolation for the theory of
     equality, in: S. Kowalewski, A. Philippou (Eds.), Tools and Algorithms for the Construction
     and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of
     the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York,
     UK, March 22-29, 2009. Proceedings, volume 5505 of Lecture Notes in Computer Science,
     Springer, 2009, pp. 413–427. URL: https://doi.org/10.1007/978-3-642-00768-2_34. doi:10.
     1007/978-3-642-00768-2\_34.
[12] J. Christ, J. Hoenicke, A. Nutz, Proof tree preserving interpolation, in: TACAS, volume
     7795 of Lecture Notes in Computer Science, Springer, 2013, pp. 124–138.
[13] J. Christ, J. Hoenicke, Proof tree preserving tree interpolation, J. Autom. Reasoning 57
     (2016) 67–95.
[14] J. Christ, J. Hoenicke, Instantiation-based interpolation for quantified formulae, in:
     N. Bjørner, R. Nieuwenhuis, H. Veith, A. Voronkov (Eds.), Decision Procedures in Software,
     Hardware and Bioware, 18.04. - 23.04.2010, volume 10161 of Dagstuhl Seminar Proceedings,
     Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2010. URL: http://drops.
     dagstuhl.de/opus/volltexte/2010/2735/.
[15] M. P. Bonacina, M. Johansson, On interpolation in automated theorem proving, J. Autom.
     Reason. 54 (2015) 69–97. URL: https://doi.org/10.1007/s10817-014-9314-0. doi:10.1007/
     s10817-014-9314-0.
[16] L. Kovács, A. Voronkov, First-order interpolation and interpolating proof systems, in:
     T. Eiter, D. Sands (Eds.), LPAR-21, 21st International Conference on Logic for Programming,
     Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC
     Series in Computing, EasyChair, 2017, pp. 49–64. URL: https://easychair.org/publications/
     paper/r2J.
[17] B. Gleiss, L. Kovács, M. Suda, Splitting proofs for interpolation, in: L. de Moura (Ed.),
     Automated Deduction - CADE 26 - 26th International Conference on Automated De-
     duction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lec-
     ture Notes in Computer Science, Springer, 2017, pp. 291–309. URL: https://doi.org/10.1007/
     978-3-319-63046-5_18. doi:10.1007/978-3-319-63046-5\_18.
[18] W. Craig, Three uses of the Herbrand-Gentzen theorem in relating model theory and



                                                15
     proof theory, J. Symb. Log. 22 (1957) 269–285. URL: https://doi.org/10.2307/2963594.
     doi:10.2307/2963594.
[19] M. P. Bonacina, M. Johansson, Interpolation systems for ground proofs in automated
     deduction: a survey, J. Autom. Reason. 54 (2015) 353–390. URL: https://doi.org/10.1007/
     s10817-015-9325-5. doi:10.1007/s10817-015-9325-5.
[20] L. Kovács, A. Voronkov, First-order theorem proving and Vampire, in: N. Sharygina,
     H. Veith (Eds.), Computer Aided Verification - 25th International Conference, CAV 2013,
     Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Com-
     puter Science, Springer, 2013, pp. 1–35. URL: https://doi.org/10.1007/978-3-642-39799-8_1.
     doi:10.1007/978-3-642-39799-8\_1.
[21] L. M. de Moura, N. Bjørner, Engineering DPLL(T) + saturation, in: A. Armando, P. Baum-
     gartner, G. Dowek (Eds.), Automated Reasoning, 4th International Joint Conference,
     IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lec-
     ture Notes in Computer Science, Springer, 2008, pp. 475–490. URL: https://doi.org/10.1007/
     978-3-540-71070-7_40. doi:10.1007/978-3-540-71070-7\_40.
[22] L. Kovács, A. Voronkov, Interpolation and symbol elimination, in: R. A. Schmidt (Ed.),
     Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction,
     Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663 of Lecture Notes in Computer
     Science, Springer, 2009, pp. 199–213. URL: https://doi.org/10.1007/978-3-642-02959-2_17.
     doi:10.1007/978-3-642-02959-2\_17.
[23] R. Bruttomesso, S. Ghilardi, S. Ranise, Quantifier-free interpolation in combinations
     of equality interpolating theories, ACM Trans. Comput. Log. 15 (2014) 5:1–5:34. URL:
     https://doi.org/10.1145/2490253. doi:10.1145/2490253.
[24] J. Christ, J. Hoenicke, A. Nutz, SMTInterpol: An interpolating SMT solver, in: SPIN,
     volume 7385 of Lecture Notes in Computer Science, Springer, 2012, pp. 248–254.




                                               16

</pre>