Spass+T is an extension of the superposition-based theorem prover Spass that allows us to enlarge the reasoning capabilities of Spass using an arbitrary SMT procedure for arithmetic and free function symbols as a black-box. We discuss the architecture of Spass+T and the capabilities, limitations, and applications of such a combination.
and passes all formulas to the base prover that the latter can handle. The correctness of such a hierarchic combination of deductive systems is obvious. In theory, conditions for completeness have been given by Bachmair, Ganzinger, Sofronie-Stokkermans, and Waldmann [1, 6]. For instance, one can get a complete hierarchic combination of provers if base and non-base vocabulary are separated using abstraction, the term ordering is chosen in such a way that base terms/atoms are smaller than non-base terms/atoms, the base prover can deal with arbitrary formulas over the base vocabulary, the extension is sufficiently complete,1 and the base theory is compact [1].
In practice, however, sufficient completeness need not hold (and cannot be checked automatically), abstraction enlarges the search space, SMT procedures for some useful theories can only deal with ground formulas (this is for instance the case for NelsonOppen combinations of arithmetic and free function symbols), and even compactness may be an issue. As an example, consider the two clauses ∀x, y. (f (x) 6= y + y) and ∀x, y. (f (x) 6= y + y + 1). If the base theory is Presburger arithmetic (linear integer arithmetic), then the conjunction of these two clauses (expressing the fact that f (x) is neither even nor odd) is inconsistent. Still any finite set of ground instances of these two formulas is consistent. Even unification modulo the base theory would not help.
An integration of first-order theorem provers and SMT procedures can therefore only be a pragmatic one: Completeness can be achieved for special classes of inputs, but not in general. If we work with non-ground problem description but ground goal formulas, then there is some hope that we can ultimately produce sufficiently many ground formulas so that the SMT procedure can find the contradiction. If we want to solve non-ground problems, in particular if we want to find solutions for variables, then the purely hierarchic approach must be supplemented by some knowledge about arithmetic that is built-in directly into Spass. 2
SPASS Spass (Weidenbach et al. [10]) is known to be one of the most advanced implementations of the superposition calculus. The superposition calculus is a refutationally complete procedure for arbitrary first-order clauses with equality, that is, it provides a semi-decision procedure for the unsatisfiability of sets of clauses. Theorem proving methods such as resolution or superposition aim at deducing a contradiction from a set of formulas by recursively inferring new formulas from given ones. New formulas are derived according to a set of inference rules. In the case of superposition, these rules are restricted versions of paramodulation, resolution, and factoring, parameterized by a reduction ordering ≻ that is total on ground expressions (that is, ground atoms and ground terms) and by a selection function S, which assigns to each clause a (possibly empty) multiset of (occurrences of) negative literals. The literals in S(C) are called selected. Selected literals, besides being negative, can be arbitrarily chosen. Ordering and selection function impose various restrictions on the possible inferences, which are crucial for the efficiency of theorem provers like Spass. Let us consider one of the inference rules of the superposition calculus as an example:
1Intuitively, sufficient completeness means that every ground term of a base sort is provably equal to a ground term consisting only of base symbols.
if (i) the literal t = t′ is strictly maximal in the first premise, (ii) no literal is selected in the first premise, (iii) either the literal ¬ s[u] = s′ is selected in the second premise or it is maximal and no literal is selected, (iv) t 6 t′, (v) s[u] 6 s′, (vi) u is not a variable, and (vii) σ is a most general unifier of t and u.
This inference rule combines the unification of t and the subterm u of s with subsequent replacement of uσ by t′σ. When we speak of a superposition inference we mean an arbitrary rule of the calculus.
Note that a clause with selected literals cannot serve as the left premise of a superposition inference, and that maximal terms are superposed either on maximal or selected literals, and a smaller term is never replaced by a larger one. Moreover, only the maximal sides of equations are replaced. The pattern of interplay between ordering restrictions and the selection function is the same for all inference rules of the calculus.
The local restrictions of the superposition inference rules are supplemented by a global redundancy criterion that allows us to discard formulas that are provably unnecessary for deriving a contradiction. 3
Spass+T consists of three modules: the theorem prover Spass, a (rather arbitrary) SMT procedure for integer or real arithmetic and free function symbols, and a module SMT-Control connecting both. The proof systems are only loosely coupled; they wait for each other only if they have completed their own task.
Spass sends three kinds of messages to SMT-Control: – all the ground formulas present in the input or derived during the saturation; – proof found (signaling that Spass has derived the empty clause); – end of file (signaling that Spass has saturated its input).
SMT-Control collects the formulas sent by Spass and repeatedly sends portions of the set of formulas to the SMT procedure,2 until one of the following events occurs: – Spass sends proof found ; – the SMT procedure detects unsatisfiability; – the SMT procedure detects satisfiability after Spass has sent end of file and the
SMT procedure has seen all the output of Spass.
The result is “proof found” in the first two cases, “no proof found” in the third one. Lacking completeness, “no proof found” does in general not imply satisfiability.
2Under the assumption that the SMT procedure works incrementally. Alternatively the SMT procedure can be restarted with increasing subsets of the set of formulas.
There are applications where we can guarantee that every base theory formula generated by Spass is ground. In this case, the very simple setup described above is already sufficient. An example is pointer data structure verification a` la McPeak and Necula [7]. In this scenario, we consider recursive data structures involving pointers to records or to nil . Record fields can either be scalar values or pointers. In the axioms used to describe the behaviour of a data structure, all variables range over pointer values (i. e., there is no quantification over scalar values). Record fields are encoded as (partial) functions, so x.data, i. e., the data field of the record that x points to, is written as data (x). McPeak and Necula require that every occurrence of such a function must be guarded by a condition that ensures that the argument is non-nil. For instance, the formula stating that the prev pointer is the inverse of the next pointer in a doubly linked list looks like ∀x. (x 6= nil ∧ next (x) 6= nil → prev (next (x)) = x), and the formula stating that the data field of any record is positive looks like ∀x. (x 6= nil → data (x) > 0).
To avoid positive disjunctions, we replace the guard formula x 6= nil by isrecord (x), obtaining ∀x. (isrecord (x) ∧ isrecord (next (x)) → prev (next (x)) = x),
∀x. (isrecord (x) → data (x) > 0).
Since the SMT procedure accepts not only the symbols of the arithmetical theory, such as +, −, · , <, or ≤, but also free function or predicate symbols, the distinction between base and non-base symbols is somewhat arbitrary – if it is useful, we may treat both theory symbols and a subset of the free symbols as base symbols. Let us therefore consider the guard predicate isrecord as the only non-base symbol in the signature. If we select the occurrences of isrecord (t) in the antecedent, we ensure that the only inferences that are possible with such clauses are (repeated) resolution steps with positive occurrences of isrecord (s). Since isrecord (s) occurs positively only in goal formulas (or formulas recursively derived from goal formulas), and since the term s is always ground in these formulas, the base formulas resulting from resolution are ground and can be passed to the SMT procedure. In effect, Spass+T mimics the derivation steps of McPeak and Necula, and the completeness result of McPeak and Necula carries over to Spass+T. 5
If non-ground theory literals are not guarded, then it can easily happen that the usual inference rules of Spass do not produce those ground instances that the SMT procedure would need to find a contradiction. Consider the following example from Boyer and Moore [3]: Let min and max be non-theory function symbols denoting the minimum and the maximum element of a list of numbers. Suppose that we want to refute ¬ (l < max (a) + k) using the assumptions l ≤ min(a) and 0 < k and the universally quantified lemma ∀x. (min(x) ≤ max (x)). Analogously to Boyer and Moore, we need an additional inference rule that computes the required ground instance of this lemma. For efficiency reasons, we restrict ourselves to instantiations where a term headed by a non-theory symbol occurs in at least one other ground clause – if a non-theory term occurs in only one clause, this clause is very unlikely to be useful to the SMT procedure, at least in linear arithmetic. We obtain the following inference rule:
if L[t] ∨ D is not ground, t is headed by a non-theory function symbol and occurs in a maximal literal L[t] immediately below a theory symbol, all function or predicate symbols occurring above t in L[t] are theory symbols or equality, C[s] is ground, σ is an mgu of s and t, and (L[t] ∨ D)σ is ground. In the example above, the theory instantiation inference l ≤ min(a)
min(x) ≤ max (x) min(a) ≤ max (a) yields the ground clause that the SMT procedure needs to derive a contradiction. There is one problem with this rule, though: The generated formula (L[t] ∨ D)σ is subsumed by the second premise L[t] ∨ D; therefore Spass will delete it again. We export it to the SMT procedure before the redundancy check, but we must also ensure that (L[t] ∨ D)σ can again be used as a first premise in a theory instantiation inference. To this end, we introduce a special new predicate symbol ground and split the inference rule into two parts:
C[s] ground (s) if C[s] is ground and s is headed by a non-theory function symbol.
Theory instantiation II
ground (s) L[t] ∨ D ground (u1) . . . ground(un) export(D′) if L[t] ∨ D is not ground, t is headed by a non-theory function symbol and occurs in a maximal literal L[t] immediately below a theory symbol, all function or predicate symbols occurring above t in L[t] are theory symbols or equality, σ is an mgu of s and t, D′ = (L[t] ∨ D)σ is ground, and u1, . . . , un are the ground terms occurring in D′ that are different from s and headed by a non-theory function symbol.
In the example above, the theory instantiation I inference and the theory instantiation II inference
l ≤ min(a) ground (min(a)) ground (min(a)) ground (max (a))
min(x) ≤ max (x) export(min(a) ≤ max (a)) cause min(a) ≤ max (a) to be exported to the SMT procedure and ensure that the clause ground (max (a)) is available for further theory instantiation II inferences within Spass.
If we select guard literals whenever possible, and if we choose the atom ordering so that non-theory predicates are larger than theory predicates, then the theory instantiation rule is used only as a last resort: It is applied only if there are no non-theory guard literals that might produce ground instances in a more restricted manner. 6
There are several reasons to supplement the external SMT procedure in Spass+T by
simplification techniques that are built-in directly into Spass+T. First of all, such
simplification techniques offer the chance to find solutions for variables, say, to replace a
clause ∀x. (¬ x + 2 = 5 ∨ p(x)) by ∀x. (¬ x = 3 ∨ p(x)) and then by p(
In Spass+T, we use a combination of additional input axioms encoding some fragment of arithmetic and specialized simplification rules dealing with the numeric part. The latter include rules for evaluation of constant numeric subexpressions, such as and where c1 and c2 are numeric constants and c0 = c1 + c2, and rules for elementary (in-)equation solving, for instance
C[c1 + c2]
C[c0] C[(t + c1) + c2]
C[t + c0] C ∨ [¬] t + c1 ∼ c2
C ∨ [¬] t ∼ c0 where c0 = c2 − c1 and ∼ is equality or an ordering relation.
All the arithmetic simplification rules we have implemented have the property that the resulting formula is smaller than the original one in any Knuth-Bendix ordering, provided that all constants have the same weight. Still it should be clear that there is some risk of losing proofs by applying arithmetic simplification. As a trivial example consider the two clauses ∀x. (p(3 · x + 4)) and ¬ p(3 · 5 + 4). These clauses are obviously contradictory, but lacking theory unification, there is no way to derive a contradiction as soon as the second clause has been simplified to ¬ p(19).
In contrast to formulas that describe the relationships between concrete numerical constants, equations such as ∀x. (x + 0 = x), ∀x. (x − x = 0), or ∀x, y. ((x − y) + y = x) are preferably added to the input as ordinary axioms. In this way they are not only available for simplification, but also for superposition or resolution inferences. In our experiments, this capability turned out to be extremely useful for refuting non-ground queries.
The integer ordering expansion rule, which is essential for some kinds of inductive proofs, is in some way a hybrid between the two cases above.
C ∨ s ≤ t
C ∨ s = t ∨ s ≤ t − 1 C ∨ s = t ∨ s + 1 ≤ t It is an inference rule, rather than a simplification rule, and it corresponds to resolution inferences with the axioms ∀x, y. (¬ x ≤ y ∨ x = y ∨ x ≤ y − 1) and ∀x, y. (¬ x ≤ y ∨ x = y ∨ x + 1 ≤ y). These are unordered resolution inferences, however, so Spass would not perform them. The integer ordering expansion rule fills this gap, but it has to be restricted, for instance by limiting applications to clauses with only one positive literal; otherwise it turns out to be too productive. 7
We have tested Spass+T both on a list of sample conjectures [8] (theorems and nontheorems) from the TPTP library [9] and on our own list of benchmark problems, mostly combining arithmetic and data structures. We used Spass+T with CVC Lite 2.5 as external decision procedure for the union of the theory of uninterpreted functions and integer arithmetic. Spass+T options were chosen identically for all benchmark problems; in particular, arithmetic simplification, theory instantiation, and (a very restricted form of) integer ordering expansion were switched on, and precedences were chosen uniformly in such a way that non-theory predicates (notably the containment relation for collections) became larger than theory predicates.3 Moreover, the following set of auxiliary axioms was supplied:
INT01 ∀X, Y. ((X − Y ) + Y = X).
INT02 ∀X. (X + 0 = X).
INT03 ∀X. (0 + X = X).
INT04 ∀X. (X < X + 1).
INT05 ∀X, Y. (X < Y → X ≤ Y ).
INT06 ∀X. (X ≤ X).
INT07 ∀X, Y. (X < Y ↔ Y > X).
INT08 ∀X, Y. (X ≤ Y ↔ Y ≥ X).
INT09 ∀X, Y. (¬ (X < Y ∧ X ≥ Y )).
INT10 ∀X, Y. (¬ (X ≤ Y ∧ X > Y )).
INT11 ∀X, Y. (X ≤ Y ∧ Y ≤ X → X = Y ).
INT12 ∀X, Y. (X − Y = X + (−Y )).
INT13 ∀X. (−(−X) = X).
INT14 ∀X. (X · 0 = 0).
INT15 ∀X. (0 · X = 0).
INT16 ∀X. (X · 1 = X).
INT17 ∀X. (1 · X = X).
INT18 ∀X. (X/1 = X).
INT19 ∀X. (X mod 1 = 0).
3Using the set DomPred option of Spass. The experiments were carried out on an office PC with a 2.40 GHz Intel Pentium 4 CPU and 512 MB RAM running Debian Linux. All times reported are wall-clock time in seconds. 7.1
The list of integer arithmetic problems in the TPTP library contains 147 theorems and 36 non-theorems [8]. Most of the problems are rather easy. The results are summarized in the following table: Theorems Non-theorems 7.2
Integer arithmetic. In addition to the TPTP list, we have developed a collection of 75 theorems mostly combining arithmetic and data structures to test Spass+T. In the following list, the second column gives the runtime of Spass+T (wall clock time in seconds) and the result, where “+” means “Proof found”, “-” means “No proof found”, and “∞” means that the time limit of 600 seconds was exceeded.
Category Number of problems:
Proof found:
Termination in less than 1 second:
Termination in 1 to 8 seconds: No proof found:
Termination in less than 1 second: Termination in 1 to 8 seconds: Non-termination: 147 1.65 + 4.77 + 0.21 + ∀X, Y, Z. (X < 5 ∧ Y < 3 ∧ X + 2 · Y > 7 → Y = 2) ∀X. (∃Y. (Y < X ∧ ¬ ∃Z. (Y < Z ∧ Z < X))) ¬ ∃X. (0 < X ∧ ∀Y. (Y < X → Y + 1 < X)) 0.15 + Integer arithmetic and collections. The formulas
COL01 ∀I.(¬ I ∈ ∅).
COL02 ∀I,S.(I ∈ add(I,S)).
COL03 ∀I,S.(¬ I ∈ remove(I,S)).
COL04 ∀I,S,J.(I ∈ S ∨ I = J ↔ I ∈ add(J,S)).
COL05 ∀I,S,J.(I ∈ S ∧ ¬ I = J ↔ I ∈ remove(J,S)). were used to axiomatize collections of integers for the following problems: (43) 0.31 + ¬ 4 ∈ add(1,add(3,add(5,∅))) (44) 0.56 + ∀S,I,J.(S = add(5,add(3,add(1,∅)))
∧ I ∈ S ∧ J ∈ S ∧ ¬ I = J → I + J < 9) EmpiricallySuccessfulComputerizedReasoning 0.36 + ∀S. (S = add (10, add (30, add (50, ∅)))
→ ∃I. (20 ≤ I ∧ I ≤ 40 ∧ I ∈ S)) Integer arithmetic and collections with counting. The formulas CCO01 ∀I. (¬ I ∈ ∅).
CCO02 ∀I, S. (I ∈ add (I, S)).
CCO03 ∀I, S. (¬ I ∈ remove(I, S)).
CCO04 ∀I, S, J. (I ∈ S ∨ I = J ↔ I ∈ add (J, S)).
CCO05 ∀I, S, J. (I ∈ S ∧ ¬ I = J ↔ I ∈ remove(J, S)).
CCO06 ∀S. (count (S) ≥ 0).
CCO07 ∀S. (S = ∅ ↔ count (S) = 0).
CCO08 ∀I, S. (¬ I ∈ S ↔ count (add (I, S)) = count (S) + 1).
CCO09 ∀I, S. (I ∈ S ↔ count (add (I, S)) = count (S)).
CCO10 ∀I, S. (I ∈ S ↔ count (remove(I, S)) = count (S) − 1).
CCO11 ∀I, S. (¬ I ∈ S ↔ count (remove(I, S)) = count (S)).
CCO12 ∀I, S. (I ∈ S → S = add (I, remove (I, S))). were used to axiomatize collections of integers with a counting operation for the following problems: ∀S. (count (remove(5, S)) ≥ 7
→ count (remove(4, S)) ≥ 6) ∀S. (count (add (5, S)) = count (add (3, S))
→ count (remove(5, S)) = count (remove(3, S)))
∀S, I. (count (S) + 1 ≥ count (add (I, S))) ∀S. (2 ∈ S ∧ count (S) = 1 → ¬ 5 ∈ S) ∀S, I, K. (K > 0 → count (S) + K ≥ count (add (I, S))) ∀S, I, K. (K > 0 → count (S) + K ≥ count (add (I, add (I, S)))) ∀S, I. (count (remove(2, S)) = 0
∧ count (remove (3, S)) = 0 → count (remove(I, S)) = 0) ∀S. (2 ∈ S ∧ 3 ∈ S ∧ count (S) = 2 → ¬ 5 ∈ S) ∀S, I. (2 ∈ S ∧ 3 ∈ S ∧ count (S) = 2 ∧ I > 3 → ¬ I ∈ S) ∀S, I, J. (I < 3 ∧ 6 < J ∧ I ∈ S ∧ J ∈ S ∧ count (S) = 2 → ¬ 5 ∈ S) (55) (56) (57) (58) (59) (60) (61) (62) (63) (64)
∃S, I. (count (S) + 1 > count (add (I, S))) 309.91 + ∃S. (count (S) = 3) ∀S, I, J, K. (I > J ∧ J > K
∧ I ∈ S ∧ J ∈ S ∧ K ∈ S → count (S) > 2) ∀S, J. (∀I. (I ∈ S → J > I)
→ count (add (J, S)) > count (S)) count (add (1, add (3, ∅))) = 2 count (add (5, remove (3, add (3, ∅)))) = 1 count (add (1, add (5, remove (3, add (2, ∅))))) = 3 ∀S, I. (count (remove(I, add (I, S))) = count (remove(I, S))) ∀S, I. (count (add (0, remove (I, add (I, S)))) = count (add (0, remove (I, S)))) Integer arithmetic and pointer data types. The formulas
PNT01 ∀X. (¬ isrecord (X) → length(X) = 0) PNT02 ∀X. (isrecord (X) → length(X) ≥ 1) PNT03 ∀X. (isrecord (X) → length(X) = length(next (X)) + 1) PNT04 ∀X. (¬ isrecord (X) → ¬ isrecord (split1 (X))) PNT05 ∀X. (isrecord (X) → isrecord (split1 (X))) PNT06 ∀X. (isrecord (X) → data(split1 (X)) = data (X)) PNT07 ∀X. (isrecord (X) ∧ ¬ isrecord (next (X))
→ ¬ isrecord (next (split1 (X)))) PNT08 ∀X. (isrecord (X) ∧ isrecord (next (X))
→ next (split1 (X)) = split1 (next (next (X)))) PNT09 ∀X. (¬ isrecord (X) → ¬ isrecord (split2 (X))) PNT10 ∀X. (¬ isrecord (next (X)) → ¬ isrecord (split2 (X))) PNT11 ∀X. (isrecord (X) ∧ isrecord (next (X)) → isrecord (split2 (X))) PNT12 ∀X. (isrecord (X) ∧ isrecord (next (X))
→ data (split2 (X)) = data(next (X))) PNT13 ∀X. (isrecord (X) ∧ isrecord (next (X))
→ next (split2 (X)) = split2 (next (next (X)))) were used to axiomatize singly linked lists with pointers and two recursive functions split1 and split2 (computing the sublists of odd-numbered and even-numbered elements of a list) for the following problems: (74) 20.02 + ∀X, Y. (isrecord (X) ∧ isrecord (next (X)) ∧ Y = next (next (X)) ∧ (2 · length(split2 (Y )) = length(Y ) − 1
∨ 2 · length(split2 (Y )) = length(Y )) → (2 · length(split2 (X)) = length(X) − 1
∨ 2 · length(split2 (X)) = length(X)))
17.18 + 7.3
∀X, Y. (isrecord (X) ∧ isrecord (next (X)) ∧ Y = next (next (X))
∧ length(split1 (Y )) + length(split2 (Y )) = length(Y ) → length(split1 (X)) + length(split2 (X)) = length(X)) Summarizing the previous section, we see that Spass+T solves 63 out of the 75 problems in our list. In order to check to what extent the mechanisms implemented in Spass+T contribute to these proofs, we have gradually disabled various features and re-run the tests. The following table shows the number of proofs found for several combinations of features:
SMT procedure
Theory instantiation
Arithmetic simplification
Auxiliary axioms
Problems solved (out of 75) + + + + + + + + + + + + + + + +
How does Spass+T compare to a system like Simplify (Detlefs, Nelson, and Saxe [4])? The automatic theorem prover Simplify was developed as the proof engine of ESC/Java and ESC/Modula-3. It handles universal quantifiers in the input by computing (hopefully) relevant instances in a similar way as the theory instantiation rule of Spass+T and analyzing the resulting formulas using SAT checking and a Nelson-Oppen combination of decision procedures. Simplify (version 1.5.4) solves 40 out of the 75 problems in our list. The difference to Spass+T is partially due to the fact that Simplify solves only four out of 23 problems that involve existential quantifiers, namely (41) and (51)–(53). Somewhat surprisingly, however, Simplify fails also for (55), (56), (59), and (68)–(74). On the other hand, due to the highly optimized implementation and the reduced search space, all problems that Simplify does solve are solved in less than one second.
It is perhaps illustrative to have a closer look at those problems that Spass+T failed
to prove. Spass+T has some support for solving non-ground equations, but it makes
no attempt to be complete in this domain, and in particular it does not use any kind of
theory unification. This accounts for most of the missed proofs in the TPTP list and in
theorems (
Theorem (19) is rather difficult for an automated system because for proving it one
has to “invent” a term that does not occur in the problem, namely f (f (Y ) + 1), and
then use transitivity. Moreover, as one might expect, Spass+T has no chance to prove
the induction theorem (26). On the other hand, an extension of the theory instantiation
rule would enable Spass+T to prove the pigeonhole-like formula ∀X, Y. (f (X) = f (Y ) →
X = Y ) ∧ 6 < f (
Even though the CCO axioms have a simple operational reading, it seems to be difficult for automated provers to detect this fact, as one can see from the poor results for straightforward computation tasks like (71) or (73). Simplify even exceeds the 600 second time limit for the simpler variants (69), (70), and (72).
There is one odd case left: Surprisingly, Spass+T succeeds to prove formula (37), if theory instantiation or integer ordering expansion are switched off, but fails to find the proof if both inference rules are switched on. It turns out that, in the latter case, Spass+T triggers a bug in CVC Lite. 7.4
8
A current snapshot of Spass+T for Linux including the benchmark problems can be downloaded from http://www.mpi-inf.mpg.de/~uwe/software/.
The development of Spass+T is ongoing work. More effort has to be spent on fine-tuning the theory instantiation rule and the arithmetic simplification rules. A more challenging extension is the implementation of subsumption checks for clauses with theory literals, which might turn Spass+T into a decision procedure for some classes of formulas. We are also looking into using Spass+T with non-numeric base theories, such as arrays, lists, or bitvectors.
Acknowledgments: We are grateful to Christoph Weidenbach and Thomas Hillenbrand for helpful discussions. [2] Clark Barrett and Sergey Berezin. CVC Lite: A new implementation of the Cooperating Validity Checker. In Rajeev Alur and Doron A. Peled, editors, Computer