Let T be an SMT solver with no theory solvers except for Quantifier Instantiation. Given a set of ifrst-order clauses S saturated by Resolution (with a valid literal selection function) we show that T is complete if its Trigger function is the same as the literal selection function. So if T halts with a ground model G, then G can be extended to a model in the theory of S. In addition for a suitable ordering, if all maximal literals are selected in each clause, then T will halt on G, so it is a decision procedure for the theory S. Also, for a suitable ordering, if all clauses are Horn, or all clauses are 2SAT, then T solves the theory S in polynomial time.
results to equational logic [
As an example of the problem faced by SMT solvers, consider the following FO theory represented by clauses, where capital letters are universally quantified variables. This example shows that even if the FO theory has no disjunction, SMT solvers already have trouble:
((), ) ¬(, )
If we give this theory to z3 [
We now consider an FO theory that contains disjunction, to discuss trigger selection:
This is another theory that z3 cannot solve when presented with ground clause (, ). The previous example only consisted of unit clauses, so there was no question of which literals to select for triggers. But in this example, we need to decide which literals to select for triggers. So we now consider three possible trigger selection strategies.
1. If we select ( (1), 1) and (2, (2)) as triggers, we show whenever an SMT solver halts without saying "unsatisfiable", the ground model it has created is actually a model of the FO theory. In fact, for a fragment of FO logic to which this theory with this selection function belongs, we show that the SMT solver is a polynomial-time decision procedure. 2. If we select ¬(1, 1) and ¬(2, 2) as triggers,3 a halting SMT solver can determine satisfiability. Unfortunately, given ground clause (, ) the procedure will not halt. 3. If we select ( (1), 1) and ¬(2, 2), then the SMT solver will return "unknown", because ground clauses (, ) and ¬( (), ()) are unsatisfiable in that theory, but the SMT solver will not generate any instances. However, if we add the FO clause ¬(3, 3) ∨ ( (3), (3)) to the FO theory, and select either literal in that clause, the SMT solver is complete.
In the first trigger selection (and the third one with the extra clause), the SMT solver creates
enough instantiations to guarantee satisfiability. Unfortunately, the instantiations will not halt
2We don’t mean to pick on z3. We also ran this on cvc5 [
Our purpose is not to create a new inference system, but to understand when existing SMT solvers could answer "satisfiable" instead of "unknown", such as the above examples. If a set of FO clauses is saturated under Resolution with a valid selection function (as defined below), we choose the literals selected during Resolution to be the triggers. If an SMT solver halts with "unsatisfiable", the problem is unsatisfiable. But if the SMT solver halts without detecting unsatisfiability, most SMT solvers would say "unknown". However, using our method of trigger selection, we can know the problem is satisfiable. Furthermore, the partial ground model that the SMT solver has constructed can be extended to a model of the FO theory. In Example 1, the FO theory is saturated. In Example 2, the first-order theory is saturated under all three selection functions, assuming that the additional clause is added in the third case.
If, in addition, a single maximum literal is selected in each clause in the saturation of the FO theory, the SMT procedure will halt, and therefore the SMT procedure is a decision procedure. Alternatively, if the order is isomorphic to , 4 then selecting all maximal literals will give a decision procedure. If, in addition, the chosen order is a polynomial ordering which is totalizable on ground terms, the SMT solver is guaranteed to decide satisfiability in polynomial time if all clauses are Horn or all clauses contain at most two literals.
In Section 2 of this paper, we give some well-known definitions and some definitions specific
to this paper. In Section 3 we define the inference rules used to model our procedure. Section 4
proves the completeness. Section 5 shows cases where we are guaranteed to have a decision
procedure and where it is guaranteed to run in polynomial time. Section 6 gives related work,
and Section 7 summarizes the paper and gives some important future work. All proofs can be
found in [
We consider a set of ground formulas modulo a set of first-order formulas, which are in
conjunctive normal form. We follow standard definitions for Resolution theorem proving [
We assume we are given a set of variables, which we represent with capital letters, and a set of uninterpreted function symbols of various arities, represented with lower case letters. An arity is a non-negative integer. Terms are defined recursively in the following way: each variable is a term, and if 1, · · · , are terms, and is of arity ≥ 0, then (1, · · · , ) is a term. If is a predicate symbol of arity , and if 1, · · · , are terms, then (1, · · · , ) is an atom. Any atom or negation of an atom is a literal. A literal is called negative if it is negated, and positive otherwise. For all literals , we define ¯ so that ¯ = ¬ and ¬¯ = . A clause is a multiset of literals, representing a disjunction of literals. If is a literal, and Γ is a set of literals, we will write ∨ Γ to represent {} ∪ Γ . We use ⊥ to represent the empty clause. We will use “− ” to denote multiset diference. For any object , define () as the set of variables in . If () = ∅ we say that is ground, otherwise we say that is non-ground.
A substitution is a mapping from the set of variables to the set of terms, which is almost everywhere the identity. We identify a substitution with its homomorphic extension. Composition of substitutions and is defined so that ( ) = ( ) for all variables . If is a substitution then ( ) = { | ̸= }, and ( ) = { | ∈ ( )}. A substitution matches to if = , and is a unifier of and , if = . is a most general unifier of and , written = (, ) if is a unifier of and , and for all unifiers of and , there is a substitution such that = for all in ( ∪ ). Given a clause , define () = { | is ground }. Given a set of clauses , let () = ⋃︀∈ ().
We assume an ordering < is a well-founded ordering which is stable, meaning that if < then < . We assume the ordering is totalizable on all ground terms and atoms. This means the ordering can be extended to an ordering that is total on ground terms. It can be extended to literals in any way such that < ¬ for all atoms . We also assume the ordering is an atom ordering meaning that for all literals and , > implies > ¯ . Clauses are compared using the multiset ordering. A literal is said to be maximum in a clause if is larger than all other literals in , and maximal in if no other literal in is larger than . An order is a polynomial ordering if each atom only has polynomially many smaller atoms.
An partial interpretation (or just interpretation) is defined as a consistent set of ground literals such that |= if and only if ∈ . Therefore, an atom is undefined in if ̸∈ and ¬ ̸∈ . This difers with some definitions of interpretations where just the true positive literals are given. Since clauses are multisets representing disjunctions, |= if ∩ ̸= ∅, otherwise is either false or undefined in . If is not ground then we say |= if |= (). If is an interpretation and is a set of clauses, then is a model of if |= for all ∈ . Interpretations 1 and 2 are compatible if there is no literal such that ∈ 1 and ¯ ∈ 2. If 1 and 2 are compatible then 1 ∪ 2 is also an interpretation, furthermore, for any literal , 1 ∪ 2 |= if and only if 1 |= or 2 |= .
Given an interpretation and a ground clause , let (, ) = { ∈ | ̸|= ¯}. If is a set of ground clauses, let (, ) = { () | ∈ ̸|= }. i.e., (, ) is created from by removing all clauses true in , and then removing all literals false in from the remaining clauses.
Example 3. Consider interpretation = {¬(), ()} where is the set of clauses in the following example: 1 : () ∨ ¬() ∨ () 2 : ¬() ∨ ¬() ∨ ()
Then (1, ) = (), and (, ) is the set consisting of the unit clause ().
We want to model an SMT solver without any theories except for a quantified FO theory in CNF, represented by clauses with universal variables. Given a set of clauses , let () be the set of all ground clauses in , and let () be the set of all non-ground clauses in . An SMT solver would build a model from (). Call that model (). For most of this paper, it will not be important how that model is built. The SMT solver will use () to instantiate the clauses of (). We will use inference rules to model the instantiation process.
Let be a function so that for each clause in (), () ⊆ and ( ()) = (), which determines which parts of are used for instantiation. Below we show how to choose triggers in such a way that when we have a model, and no more instantiations can be performed, we can deduce that is satisfiable. The Instantiation rule is used to instantiate non-ground clauses based on a ground interpretation .
-Instantiation: where
1 ∨ · · · ∨ (1 ∨ · · · ∨ ∨ Γ ∨ Γ) 1. 1 ∨ · · · ∨ ∨ Γ ∈ (), 2. (1 ∨ · · · ∨ ∨ Γ) = {1, · · · , } 3. there exists ′1 · · · ′ in such that ¯ = ′ for all 1 ≤ ≤
We do not consider equality, so we only require to be a matcher, not an -matcher. SMT solvers allow triggers to be subterms of a literal. But to reduce the number of instantiations, we only use entire literals as triggers. Furthermore, we only need to match a ground literal in the model onto the complement of a non-ground literal. This allows the instantiation rule to be more restrictive than is usually the case for trigger-based instantiation in SMT. Finally, SMT solvers allow for diferent possible sets of triggers for the same clause. We only require one set of triggers for each clause.
A set of clauses is saturated by Instantiation if either () is unsatisfiable or there exists a model () of () such that every conclusion of an ()-Instantiation inference is in .
1 : ¬(1, 1) ∨ ( (1), 1) 2 : ¬(2, 2) ∨ (2, (2))
3 : ¬( (), ())
We define 1 so that 1(1) = {( (1), 1)} and 1(2) = {(2, (2))}. Given the model 1 = {¬( (), ())} of 3, we apply the Instantiation rule to create the clause 4 = ¬( (), ) ∨ ( (), ()). Then, we can create a new model 2 = {¬( (), ()), ¬( (), )} of 3 and 4. Instantiation then creates 5 = ¬(, ) ∨ ( (), ), and we create a new model 3 = {¬( (), ()), ¬( (), ), ¬(, )} of 3 and 4. These five clauses are now saturated by Instantiation.
Consider the same set of three clauses with a diferent trigger function 2 defined so that 2(1) = {( (1), 1)} and 2(2) = {¬(2, 2)}. Let 1 be the same model as before. There are no instantiations, so the three clauses are saturated by Instantiation. Suppose we also had the clause 6 = (, ). Then the model of the clauses would be 4 = {¬( (), ()), (, )}. The set of clauses {1, 2, 3, 6} is again saturated by Instantiation, although it is unsatisfiable. In other words, this was not a good choice of triggers.
The theory {(1), ¬(2)}, with no ground clauses, is unsatisfiable, but no instantiations exist. So there cannot be a set of triggers that guarantees completeness for all formulas. To address this problem, we require the non-ground clauses to be saturated under the Factoring and Resolution inference rule defined below. These inference rules depend on a selection function, which selects the literals in each clause that may be used in an inference. A selection function maps a clause to a subset of its literals, just like the trigger function. A selection function is valid if, for each clause and for each ⊆ () with ( ) ̸= (), either () − contains all maximal literals in − , or () − contains a negative literal.
Before we give an intuition of this definition, let us give some properties: Proposition 1. For any clause and valid selection function , (()) = (). Proposition 2. Let be a selection function such that for all , (()) = () and either (1) () contains only negative literals or (2) () is a singleton set containing the maximum literal in . Then is a valid selection function.
Selection functions normally select all maximal literals or a negative literal. We additionally require () to contain all the variables in . We also require that if some of the literals from the selected set are removed from the clause, without covering all the variables, the remaining selected set must contain all maximal literals in the remaining clause or a negative literal. In the completeness proof, we will filter our clauses by the ground model, and must ensure that the filtered clauses still have a valid selection function.
In Example 4 with trigger function 1, if the selection function is the same as the trigger function, it is easy to construct an ordering where the selected literal is the largest in 1 and 2. So this is a valid selection function. If the trigger function is 2, the same is true for 1. For 2, 2(2) contains only negative literals, so the selection function is valid.
Let us look at one more example. Consider the following set of clauses, with an ordering where (1) > (2) > (3) for all terms 1, 2, 3.
1 : ¬(1) ∨ ¬(1) 2 : (2) ∨ ¬(2) 3 : ¬(3) ∨ (3) 4 : (4) ∨ (4) ∨ ¬(4)
Let 1 be the selection function such that 1(1) = {¬(1)}, 1(2) = {¬(2)}, 1(3) = {(3)}, and 1(4) = {¬(4)}. 1 is not valid, because 1(4) does not contain all the variables of 4. So let 2 be a selection function identical to 1 on the ifrst three clauses, but 2(4) = {(4), ¬(4)}. This selection function is also not valid because in clause 4 if we let = {¬(4)}, then 2(4) − = {(4)}, and (4) is neither maximal nor negative in (4) ∨ (4). Finally we define 3 to be the same as 1 on the first three clauses but 3(4) = {(4), ¬(4)}. This selection function is valid.
Given a valid selection function, our inference system will consist of three inference rules. We defined Instantiation above. Below we define Resolution and Factoring: ∨ Γ ¬ ∨ ∆ (Γ ∨ ∆) ∨ ∨ Γ ( ∨ Γ) ∈ (), (3) is selected in ∨ Γ , (4) ¬ is selected where (1) ∨ Γ ∈ () , (2) ¬ ∨ ∆ in ¬ ∨ ∆ , and (5) = (, ).
where (1) ∨ ∨ Γ ∈ () , (2) is selected in ∨ ∨ Γ , and (3) = (, ).
When applying Resolution and Factoring, it is important to remove redundant clauses. In particular, implementations remove subsumed clauses and tautologies.
Definition 1. A clause subsumes a clause if there is a substitution such that ⊆ . A clause is a tautology if there is an atom such that ∈ and ¬ ∈ . A set of clauses (possibly infinite) is saturated by Resolution and Factoring if the conclusion of every Resolution and Factoring inference in is either a tautology or is subsumed in . is completely saturated if is saturated by Instantiation and saturated by Resolution and Factoring.
In Example 4, with selection and trigger function 1, the set {1, 2, 3, 4, 5} is completely saturated. If the selection and trigger function are 2, the set {1, 2, 3} is saturated by Instantiation but not saturated by Resolution and Factoring. The result of a Resolution between 1 and 2 is 7 = ¬(7, 7) ∨ ( (7), (7)). We extend the selection and trigger function to 7. Suppose we extend 2 so that 2(7) = {( (7), (7))}. Then an instantiation will give us 8 = ¬(, ) ∨ ( (), ()). Extending the model to {(, ), ( (), ())} allows us to see that {1, 2, 3, 7, 8} is completely saturated.
In Example 5, if we add a ground clause 5 = (), then {1, 2, 3, 4, 5} is completely saturated under selection function 2, because every Resolution inference yields a tautology, even though the set is unsatisfiable. So if we had only required valid selection functions to select a negative literal or all maximal literals in each clause, we could not prove completeness, even if we additionally required that the selected literals contain all the variables in the clause. Using selection function 3, the set of clauses is not saturated under Resolution and Factoring.
In this section we will prove the completeness of our inference system. Given a set of clauses , the first step in our completeness proof is to filter the ground instances of () with a model () of (). Let () = ((()), ()).
We explain () with an example, where we write () to abbreviate applied times to . Note that is not saturated under Instantiation in this example, although in the proof we only construct () for completely saturated sets.
Example 6. Let () = {¬( ) ∨ ( ( ))}. Suppose that we have the model () = {¬( ()), ( 3())} of (). Then (()) = {¬( ()) ∨ ( +1()) | ≥ 0}. So () is the set of clauses {¬(), ( 4())} ∪ {¬( ()) ∨ ( +1()) | ≥ 4}.
Instances of subsumed clauses and tautologies in are also subsumed clauses and tautologies in (), if they exist in ().
Lemma 1. Let be a clause in . Let be a ground substitution. Let ′ = (, ()). Then (a) If is a tautology then either ′ is not in () or ′ is a tautology. (2) If is subsumed in then either ′ is not in () or there is a clause ′ in () such that ′ ⊆ ′.
Subsumption and tautology deletion are instances of the concept of redundancy,5 A clause may be redundant in but () not redundant in (), so our filtering technique does not cover redundancy in full. However, subsumption and tautology deletion are what is mainly used in practice to control saturation.
Example 7. Let be a set of clauses such that () = {( ) ∨ ( ), ¬( ), ¬( ) ∨ ( )} with () = {()} and an ordering such that () < () < () for all terms , , . Then ¬( ) ∨ ( ) is implied by smaller clauses ( ) ∨ ( ) and ¬( ). But when we apply filtering, we get clauses {() ∨ (), ¬(), ()}, and () is not implied by smaller clauses.
To prove completeness, we will let be a completely saturated set of clauses with = . We show that if ⊥ is not in and () is satisfiable, then a model of () can be constructed which is compatible with the model of ().
First we need some definitions. For a set of clauses , let < = { ∈ | < } be the set of clauses in that are smaller than . We will create an interpretation from a set of positive literals. So, given a set of positive literals and a set of literals , we define ( , ) = ∪ {¬ | ̸∈ , ( − ) ∩ {, ¬} ̸= ∅} In other words, it is the interpretation where all the atoms in are true, and every atom in that has not been made true in is false. For each clause ∈ (), we will define < , < and co-recursively.
Let () be the clause set defined above, and be a clause in (). 1. Define < as the set of positive literals ⋃︀∈ ()< , where is defined below. 2. Define () = ⋃︀∈ () , the union of all the defined below. 3. Let < = (< , ∪ ⋃︀ ()< ), which means that < is the interpretation that makes true all the atoms in < , and makes false all other atoms in clauses of () that are smaller than or equal to . 4. Similarly, let () = ( (), ⋃︀ ()).
Simultaneously we define = {} for atom if (1) < ̸|= , (2) is the largest literal in , (3) is selected in , and (4) only occurs once in . Otherwise = ∅.
If = {}, we say that produces .
The completeness proof is similar to the standard proof of completeness of Resolution, except we deal with filtered clauses, so lifting is more complex. Also, we use Instantiation when the ifltering removes all the selected literals. The next lemma follows from the definition of .
Lemma 2. Let be a clause in (). Let be a literal in . Then (1) If is not maximum in then () |= if and only if < |= . (2) If produces then ∈ ().
For the proof below, we will assume that for every ∈ and ∈ , where ′ = (, ()), then is selected in if and only if ∈ ′ and is selected in . Theorem 1. Let be a valid selection function with = . Suppose that is completely saturated and ⊥ ̸∈ and () is satisfiable. Let () be a model of () such that is saturated by ()-Instantiation. Then () |= () where () = ((()), ()). Proof Sketch 1. As usual in model construction proofs, we prove that () is a model of () by showing that a least counterexample leads to a contradiction. As usual, if a negative is selected, Resolution leads to a smaller counterexample. If the largest positive is selected, Factoring leads to a smaller counterexample. However, all selected literal may have been filtered out. In which case, Instantiation leads to a contradiction. In all cases, the filtering process allows ground inferences to be lifted.
We can combine () with () to get a model of .
Corollary 1. Let be a valid selection function with = . Suppose that is completely saturated and ⊥ ̸∈ and () is satisfiable. Let () be a model of () such that is saturated by ()-Instantiation. Let () = ((()), ()). Then () is compatible with () and () ∪ () |=
Next we assume the clauses are saturated by Resolution and Factoring, and find cases where they can be further finitely saturated by Instantiation. Then SAT Solving plus Instantiation is a decision procedure for the theory of (). For example, if the selection function selects a single maximum literal in each clause.
Theorem 2. Let be a valid selection function such that a single maximum literal is selected in each clause of (), with = . Suppose that is saturated by Resolution and Factoring. Then can be saturated by Instantiation in finite time.
We also get a decision procedure if the ordering used is order isomorphic to . Theorem 3. Let be a valid selection function such that all maximal literals are selected in each clause, with an ordering that is order isomorphic to . Suppose that = and that is saturated by Resolution and Factoring. Then can be saturated by Instantiation in finite time.
If the selection function selects a negative literal, then the Instantiation rule may not halt. Example 8. Consider Example 4 where (1) = {¬(1, 1)} and (2) = {¬(2, 2)}. This is saturated by Resolution and Factoring, but Instantiation with ground clause (, ) creates infinitely many clauses.
Even if all maximal literals are selected in each clause, there may still be infinitely many instantiations, as in the following theory, with an ordering such that () > () for all and .
: ¬( ) ∨ ¬( ) ∨ ( ( ))
Suppose that () = {¬( ), ¬( )}. This is a valid selection function, and ( ) is the maximum literal. But suppose we have () and () in the ground model. Instantiation will create ( ()) for all , all literals smaller than ().
We would also like to determine conditions where Instantiation halts in polynomial time, given that is already saturated by Resolution and Factoring. This requires that only polynomially many instantiations are computed, and that the SAT solver runs in polynomial time.
To get polynomial time results, we must examine the details of an SMT solver. We assume
the SMT solver is based on a CDCL SAT solver [
For Horn clauses, we assume that the initial decision about an atom is to make it false. It is well-known that satisfiability of ground Horn clauses can be decided in polynomial time, but we are not aware of any results that CDCL SAT solvers solve Horn clauses in polynomial time. Theorem 4. Let < be a polynomial ordering. Let be a valid selection function such that all maximal literals are selected in each clause of (), with = . If is saturated by Resolution and Factoring, and only contains Horn clauses, then the saturation of by CDCL SAT solving and Instantiation runs in polynomial time if the initial decision for the truth value of ground atoms is false. Therefore SAT solving plus Instantiation is a polynomial time decision procedure for the theory of (), if all ground clauses are Horn clauses.
Clause learning is crucial for 2SAT. Satisfiability of 2SAT can be decided in polynomial time, but we have not seen any results that CDCL SAT solvers solve 2SAT in polynomial time. Theorem 5. Let < be a polynomial ordering. Let be a valid selection function such that all maximal literals are selected in each clause of (), with = . If is saturated by Resolution and Factoring, and contains no clauses with more than two literals, then the saturation of by CDCL SAT solving plus Instantiationin runs in polynomial time. Therefore CDCL SAT solving plus Instantiation is a polynomial time decision procedure for the theory of (), if all ground clauses contain at most two literals.
Example 4 is Horn and 2SAT. Consider selection and trigger function 1, with (1, 2) ≤ (1, 2) if 1 is a subterm of 1 and 2 is a subterm of 2. We do the same for . CDCL SAT solving plus Instantiation will solve this theory in polynomial time.
The paper [
Other papers suggest other approaches to quantifiers instead of triggers. Some successful
approaches are Model-Based Quantifier Instantiation [
Other papers have used Saturation under Ordered Resolution [
Another technique is for an SMT solver to call an FO theorem prover [32, 33, 34]. Our method is diferent in that we do not need a first-order theorem prover after saturation of the FO clauses.
We analyzed the completeness of the trigger selection function for SMT solvers with an FO theory and no other theories. If is saturated by Resolution and Factoring with a valid selection function identical to the trigger function, then Saturation by Instantiation gives a model of the ground clauses, that is also a model of those clauses modulo the first-order theory. Saturation by Instantiation is guaranteed to halt if the Selection function selects a single maximum literal in each clause, or if all maximal clauses are selected using an ordering isomorphic to . If it is also a polynomial ordering, then Saturation by Instantiation is guaranteed to halt in polynomial time if all clauses are Horn Clauses, or if all clauses contain at most two literals.
SMT solvers often return "unknown" on problems that seem to be easily shown to be satisfiable. We hope implementers of SMT solvers will use our results to return "satisfiable" in more cases. It requires no change to the SMT process. The only change is in the pre-processing, where the SMT solver checks if the FO classes are saturated by a valid selection function, and uses the identical trigger function. At the end, if no contradiction is found, the SAT solver will return "satisfiable", and also return a model modulo extendable to the FO theory.
We have implemented an SMT solver that, given a satisfiable saturated first-order theory, will detect satisfiability and return a ground model. We experimented with our SMT solver using some first-order theories presented in the appendices. Since this is a new SMT solver, we don’t expect it to be competitive in speed with existing SMT solvers. However, this paper is not about increasing the speed of an SMT solver. It is about making SMT solvers more precise.
We plan lots of future work on this subject. To make this useful, we need to extend the results to more theories. We are working on extending it to equality with uninterpreted function symbols. Later work will be to extend it to other specialized theories.
Even in the non-equational case, there are many unanswered questions. For example, can this be extended to theories which cannot be saturated under Resolution. These results basically give Herbrand models. There may be ways to use other models to strengthen these results. There are several more detailed results that are not answered in this paper. Does the proof technique work for all cases of redundancy, not just subsumption and tautology deletion? Other decision procedures may be possible by loosening the restrictions on the ordering. Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, volume 3632 of Lecture Notes in Computer Science, Springer, 2005, pp. 219–234. URL: https://doi.org/10.1007/11532231_16. doi:10.1007/11532231\_16. [27] C. Ihlemann, S. Jacobs, V. Sofronie-Stokkermans, On local reasoning in verification, 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. 265–281. URL: https://doi.org/10.1007/978-3-540-78800-3_19. doi:10.1007/978-3-540-78800-3\_19. [28] S. Jacobs, Incremental instance generation in local reasoning, in: A. Bouajjani, O. Maler (Eds.), Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, Springer, 2009, pp. 368–382. URL: https://doi.org/10.1007/978-3-642-02658-4_29. doi:10.1007/978-3-642-02658-4\_29. [29] H. Ganzinger, K. Korovin, New directions in instantiation-based theorem proving, in: 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, IEEE Computer Society, 2003, pp. 55–64. URL: https://doi.org/10. 1109/LICS.2003.1210045. doi:10.1109/LICS.2003.1210045. [30] K. Korovin, iprover - an instantiation-based theorem prover for first-order logic (system description), in: A. Armando, P. Baumgartner, G. Dowek (Eds.), Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 1215, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, Springer, 2008, pp. 292–298. URL: https://doi.org/10.1007/978-3-540-71070-7_24. doi:10.1007/ 978-3-540-71070-7\_24. [31] K. Bansal, A. Reynolds, T. King, C. W. Barrett, T. Wies, Deciding local theory extensions via e-matching, in: D. Kroening, C. S. Pasareanu (Eds.), Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, Springer, 2015, pp. 87–105. URL: https://doi.org/10.1007/978-3-319-21668-3_6. doi:10.1007/978-3-319-21668-3\_6. [32] C. Lynch, Q. Ta, D. Tran, SMELS: satisfiability modulo equality with lazy superposition, J. Autom. Reason. 51 (2013) 325–356. URL: https://doi.org/10.1007/s10817-012-9263-4. doi:10.1007/s10817-012-9263-4. [33] L. M. de Moura, N. S. Bjørner, Engineering DPLL(T) + saturation, in: A. Armando, P. Baumgartner, G. Dowek (Eds.), Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture 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. [34] A. Voronkov, AVATAR: the architecture for first-order theorem provers, in: A. Biere, R. Bloem (Eds.), Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, Springer, 2014, pp. 696–710. URL: https://doi.org/10.1007/978-3-319-08867-9_46. doi:10.1007/ 978-3-319-08867-9\_46.