Proofs and Refutations, and Z3

Abstract

Z3 [3] is a state-of-the-art Satisfiability Modulo Theories (SMT) solver freely available from Microsoft Research. It solves the decision problem for quantifier-free formulas with respect to combinations of theories, such as arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is used in various software analysis and test-case generation projects at Microsoft Research and elsewhere. The requirements from the user-base range from establishing validity, dually unsatisfiability, of firstorder formulas; to identify invalid, dually satisfiable, formulas. In both cases, there is often a need for more than just a yes/no answer from the prover. A model can exhibit why an invalid formula is not provable, and a proof-object can certify the validity of a formula. This paper describes the proof-producing internals of Z3. We also briefly introduce the model-producing facilities. We emphasize two features that can be of general interest: (1) we introduce a notion of implicit quotation to avoid introducing auxiliary variables, it simplifies the creation of proof objects considerably; (2) we produce natural deduction style proofs to facilitate modular proof re-construction.

Introduction

1. We define a notion of implicit quotation that allows us to encode a Tseitsin’ style clausification without introducing auxiliary symbols. Other proof-producing SMT systems that we are aware of [ 18 ], [ 19 ], [ 2 ], [ 22 ], introduce auxiliary symbols (such as proxy literals) during clausification and other transformations. Such symbols can impede optimizations in the theory solvers (we provide an example in Section 3.3.2 where we can avoid introducing extra Simplex Tableaux rows) and make proof re-construction more involved. as we adapt a natural deduction style calculus. This contrasts with existing proof-producing SAT solvers that generate resolution proofs directly [ 10, 6, 21 ]. We are obviously not the first to use natural deduction in the context of SMT, for example, [ 9 ], investigates efficient proof checking of natural deduction style proofs by implementing inference rules as rewrites. 3. We also do not attempt to specify all inference rules from a smaller set of axioms. Instead we rely on proof checking to be able to carry out a limited set of inferences, or refine proofs in a separate pass. This choice obviously reflects a trade-off between the requirements on the solver vs. the proof checker. Our own experience has been that the coarse granularity has in fact been sufficient in order to catch implementation bugs. Future work includes investigating whether this approach is practical in the context of proof checkers based on trusted cores [ 1 ].

Preliminaries

Terms and Formulas

Z3 uses basic multi-sorted first-order terms. Formulas are just terms of Boolean sort, and terms are built by function application, quantification, and bound variables. Sorts range over a finite denumerable set of disjoint primitive sorts. To summarize s 2 Sorts ::= t 2 Terms ::=

Boolean j Int j Proof j : : : f (t1; : : : ; tn) x 8x : s : t j 9x : s : t function application bound variable quantification j j There a a few built-in sorts, such as Boolean, Int, Real, BitVec[n] (for each n, an n-bit bit-vector), and Proof. The Proof sort is used for proof-terms. Terms can be annotated by pragmas. For example, quantifiers are annotated with patterns that control quantifier instantiation. Function symbols can be both interpreted and uninterpreted. For example, numerals are encoded using interpreted functions. Function symbols also have attributes, such as to indicate whether they are associative and/or commutative. Note that there are no binding operators other than universal and existential quantification. A number of function symbols are built-in to the base theory. We will introduce the set of proof-constructing terms as we explain their origination, but here let us summarize the main pre-declared function symbols. We use the usual infix symbols ^; _; !; $ for Boolean conjunction, disjunction, implication and bi-implication. For each sort s there is an equality relation ': s s ! Boolean. The relation : Boolean Boolean ! Boolean is used in proof terms. A proof of j y establishes that j is equisatisfiable with y. In other words, if we close j and y by second-order existential quantification of all Skolem functions and constants, we obtain equivalent formulas. 2.2

Proof Terms

Proof objects are also represented as terms. So a proof-tree is just a term where each inference rule is represented by a function symbol. For example, consider the proof-rule for modus ponens: .

.. p modus ponens y ! jj . . . q y In the rule, p is a proof-term for y ! j, and q is a proof for y. The resulting proof-term for j is then mp(p; q; j). We will later elaborate on the function symbols for building basic proof terms that are available in Z3.

Every proof term has a consequent, the formula that the proof establishes. It is always the last argument in our proof terms. To access the consequent we will use the notation con(p). For example, con(mp(p; q; j)) = j. 3 3.1

Proofs

Overview

Z3 applies multiple stages when attempting to verify a formula. First formulas are simplified using a repository of simplification rules. The result of simplification is then converted into an internal format that can be processed by the solver core. We refer to this phase as internalization. The core comprises of a SAT solver that performs Boolean search and a collection of theory solvers. The solver for equality and uninterpreted function symbols (congruence closure) features predominantly as a theory solver in Z3 as it dispatches constraints between the SAT solver and other theories.

Input formula

Simplifier (3.2)

Internalizer (3.3) SAT solver (3.4.1)

Theory Core (3.4.2,3.4.3)

As the figure illustrates, we will describe the various modules in the following sections, as we introduce the proof terms that are produced as a side effect of the modules.

The figure does not reflect the full extent of Z3. We will not be elaborating on proof objects for non-ground formulas in this paper. Z3 does produce proof objects for non-ground formulas. The required machinery introduces judgments stating equi-satisfiability of formulas. Furthermore, Z3 contains a module that produces and integrates proofs in a superposition calculus [ 4 ]. The proof terms are the usual superposition inferences [ 12 ]. That material is beyond the scope of this paper. 3.2

Simplification Rewriting

In a first phase, formulas are simplified using a rewriting simplifier. The simplifier applies standard simplification rules for the supported theories. For example, terms using the arithmetical operations, both for integer, real, and bit-vector arithmetic, are normalized into sums of monomials. A single axiom called rewrite is used to record the simplification steps. rewrite(t ' s), rewrite(j $ y) A proof for a local rewriting step that converts t to s or j to y. The head function symbol of t is interpreted. Sample instances of this proof object are: rewrite(x + 0 ' x), rewrite(x + x ' 2 x), and rewrite((j _ false) $ j).

Notice that we do not axiomatize the legal rewrites. Instead, to check the rewrite steps, we rely on a proof checker to be able to apply similar inferences for the set of built-in theories: arithmetic, bit-vectors and arrays. 3.3

Internalization

Internalization is the process of translating an arbitrary formula j into a normal form that can be consumed by efficient proof-search procedures. We will discuss two internalizations: clausification and conversion of arithmetical constraints into a format that can be processed using a global Simplex tableau. Internalization often introduces auxiliary variables that are satisfiability preserving definitional extensions of the original problem. We will introduce a simple, but apparently unrecognized, technique of implicit quotation to allow us introducing these definitional extensions, but at the same time take advantage of the fact that the auxiliary variables can be viewed directly as terms they are shorthand for. The technique of implicit quotation makes the proof extraction process fairly direct. 3.3.1

Clausification

Tseitsin’s clausal form conversion algorithm can be formulated as a procedure that works by recursive descent on a formula and produces a set of equi-satisfiable set of clauses. A simple conversion algorithm introduces one fresh name for each sub-formula, and defines the name using the shape of the sub-formula. We here recall the basic idea by converting and-or formulas into CNF.

cnf (j) = let (`; F) = cnf 0(j) in ` ^ F cnf 0(`) = (`; true) cnf 0(:j) = let (`; F) = cnf 0(j) in (:`; F) cnf 0(j ^ y) = let (`1; F1) = cnf 0(j); (`2; F2) = cnf 0(y) in

(p; F1 ^ F2 ^ (:`1 _ :`2 _ p) ^ (:p _ `1) ^ (:p _ `2)) p is fresh cnf 0(j _ y) = let (`1; F1) = cnf 0(j); (`2; F2) = cnf 0(y) in (p; F1 ^ F2 ^ (`1 _ `2 _ :p) ^ (p _ :`1) ^ (p _ :`2)) p is fresh ` is a literal More sophisticated CNF conversions that do not introduce fresh names for all sub-formulas exist [ 14 ]. They control the number of auxiliary literals and clauses introduced during clausification.

Z3 does not introduce auxiliary predicates during internalization of quantifier-free formulas. Instead, it re-uses the terms that are already used for representing the sub-formulas. Thus, instead of introducing a fresh variable p, in the CNF conversion of j _ y, we treat the term j _ y as a literal. To clarify that a sub-formula plays the roˆle of a literal below, we quote it. So the literal associated with j _ y is dj _ ye. So the CNF conversion of j _ y produces the pair:

(dj _ ye; F1 ^ F2 ^ (`1 _ `2 _ :dj _ ye) ^ (dj _ ye _ :`1) ^ (dj _ ye _ :`2)) It may appear that we need to justify the auxiliary clauses (`1 _ `2 _ :dj _ ye), (dj _ ye _ :`1), and (dj _ ye _ :`2) by appealing to the equi-satisfiablility, but the justification for these clauses happens in fact to directly use equivalence. First note that it follows by induction on the clausification algorithm that `1 is equivalent to j and `2 is equivalent to y. Each of the auxiliary clauses introduced during clausification is therefore justified as propositional tautologies. Only limited propositional reasoning is required to justify these. The proof terms corresponding to the auxiliary clauses are tagged as definitional axioms. For example, the axiom dj _ ye _ :j is represented by the term def axiom((j _ y) _ :j).

We introduced quotation here to clarify in which context logical connectives were to be used. Our implementation in Z3 does not use quotation at all. 3.3.2

Arithmetic

Implicit quotation is also used when introducing auxiliary variables for theories, such as the theory for linear arithmetic. Let us recall how the Simplex solver in Z3 works. Following [ 5 ], a theory solver for linear arithmetic, and integer linear arithmetic can be based on a Simplex Tableau of the form: where B and N denote the set of basic and nonbasic variables, respectively. The sets B and N are assumed disjoint, and each basic variable occurs in exactly one row. Thus, the values of basic variables are determined by the values of the non-basic variables. In addition to this tableau, the solver state stores upper and lower bounds li and ui for every variable xi and a mapping b that assigns a rational value b (xi) to every variable xi. The bounds on nonbasic variables are always satisfied by b , so the following invariant is maintained by the tableau operations xi '

å xj2N

ai jx j xi 2 B; 8x j 2 N ; l j b (x j)

u j: 8x j 2 B; l j b (x j) u j: (1) (2) (3) (4) (5) (6) (7) A tableau is satisfied if the same inequalities hold for the basic variables: Bounds constraints for basic variables are not necessarily satisfied by b , so for instance, it may be the case that li > b (xi) for some basic variable xi, but pivoting steps can be used to fix bounds violations, or detect an unsatisfiable tableau.

Formally, Simplex-based solvers for linear arithmetic can interface with Boolean combinations of inequalities by introducing one slack variable and a tableau row for every (maximal) linear arithmetic sub-term in a formula. For example, it is by now common for SMT solvers to transform problems of the form: sup(ar) := inf(ar) :=

å xj2N +

å xj2N + ar ju j + ar jl j +

å xj2N

å xj2N ar jl j ar ju j to the following equi-satisfiable formula: [(x + y > 2) ^ (2x y < 2)] _ [( f (z + x)

5) ^ z < 3] [(s1 > 2) ^ (s2 < 2)] _ [( f (s3)

5) ^ z < 3] ^ s1 ' x + y ^ s2 ' 2x y ^ s3 ' z + x The definitions for the slack variables translate into rows in a Simplex tableau. If we represent s1 by the quotation dx + ye, and s2 by d2x ye, and s3 by dz + xe, we observe directly that the additional equalities are tautologies and therefore have trivial justifications. Furthermore, all Simplex tableau operations, including pivoting, are equivalence preserving (pivoting replaces equals for equals, and divides rows by constants), so the justifications for the Simplex rows remains a matter of expanding quotations and checking equalities using linear arithmetic. The above observation can be used to reconstruct proofs from unsatisfiable tableaux in a direct manner. In contrast, [ 2 ] proposed an encoding of arithmetical constraints by introducing slack variables for potentially every arithmetical subterm (including potentially a slack variable for z in z < 3). The slack variables allowed for tracking explanations and extracting proofs from infeasible tableaux.

We now explain how proofs are extracted from unsatisfiable tableaux without modifying the translation phase. With a tableau row of the form (1) associate the suprema and infima of implied by the coefficients, namely, let ar be the coefficients from the row and l j and u j be the lower and upper bounds that are asserted by the literals x j u j and l j x j, then: where N = fx j j ar j < 0g, and N + = fx j j ar j > 0g; and as usual, we set sup(ar) = ¥ if either some x j 2 N +, u j = ¥, or for some x j 2 N , l j = ¥.

Then an unsatisfiable tableau can be identified by an infeasible row r, where ur < inf(ar) and xr ur is asserted, or lr > sup(ar) and lr xr is asserted:

Corresponding to an infeasible row, we can extract a theory conflict by accumulating the bounds that were used to derive a contradiction. So for example, in case of ur < inf(xr), the conflict clause is of the form :(xr ur) _ :(l j

x j) _ _ xj2N +

_ xj2N :(x j u j) (8) (9) It is now simple to prove the conflict clause: xr ' åxj2N ar jx j lr1

xr1; xr1 2 N + xr (åxj2N ar jx j) ar1xr1 + ar1lr1 xr (åxj2N ar jx j) ar1xr1 + ar1lr1 xr2

ur2; xr2 2 N ar2xr2 + ar2ur2

: : : xr

inf(ar) lemma :(xr

W ur) _ xj2N + :(l j ? x j) _ W xj2N xr

ur :(x j u j) (9) The left-most antecedent is a tautology in the theory of linear arithmetic, the other antecedents are hypotheses. The lemma inference rule collects (see Section 3.4) the disjunction of the negated hypotheses used for deriving ?. The intermediary inferences correspond to basic inequality propagation. Our implementation in Z3 only produces the theory lemma directly without listing the equality corresponding to the infeasible row. 3.4

Modular Proofs

A basic underlying principle for composing and building proofs in Z3 has been to support a modular architecture that works well with theory solvers that receive literal assignments from other solvers and produce contradictions or new literal assignments. The theory solvers should be able to produce independent and opaque explanations for their decisions.

Conceptually, each solver acts upon a set of hypotheses and produce a consequent. The basic proofrules that support such an architecture can be summarized as: hypothesis, that allow introducing an assumption, lemma, that eliminates hypotheses, and unit resolution that handles basic propagation. We say that a proof-term is closed when every path that ends with a hypothesis contains an application of rule lemma. If a term is not closed, it is open. To summarize, these core rules are: hypothesis(j) Mark j as a hypothesis. The resulting proof term is open. lemma(p; :j1 _ : : : _ :jn) The proof term has one antecedent p such that con(p) = false, but p is open with hypotheses j1; : : : ; jn. The resulting proof term is closed. unit resolution(p0; p1; : : : ; pn; y1 _ : : : _ ym) Where con(p0) = j1 _ : : : _ jn _ y1 _ : : : _ ym, con(p1) = :j1; : : : con(pn) = :jn.

We will next describe how these rules integrate within a DPLL(T ) architecture. 3.4.1

Proofs from DPLL(T )

The propositional inference engine in Z3 is based on a DPLL(T ) architecture. We refer to [ 13 ] for an exposition on a basic introduction on DPLL(T ) as a transition system. The main points we will use is that DPLL(T ) maintains a state of the form M jj F during search, where M is a partial assignment of the atomic predicates in the formula F. Furthermore, we assume F is in conjunctive normal form. The search keeps assigning atoms in M based on unit propagation, theory propagation (for example x > 3 implies that x > 0 by the theory of arithmetic), and guesses (also called decisions) until either it reaches a state where the assignment satisfies all clauses in F, or some clause in F contradicts the assignment in M.

The DPLL(T ) proof search method lends itself naturally to producing resolution style proofs. Systems, such as zChaff, and a version of MiniSAT [ 10, 6, 21 ], produce proof logs based on logging the unit propagation steps as well as the conflict resolution steps. The resulting log suffices to produce a propositional resolution proof. This approach works even though the SAT solver can choose to restart or garbage collect learned conflict clauses that were produced during search.

The approach taken in Z3 bypasses logging, and instead builds proof objects during conflict resolution. With each clause we attach a proof. Clauses that were produced as part of the input have proofs that were produced from the previous steps. A clause that is produced during conflict resolution depends on some state of the partial model M. In particular, the learned clause is contradictory with some subset of the decision literals in M, either directly because the learned clause contains decision literals, or because the learned clause contains a literal that was obtained by propagation. Given a conflict clause C : `1 _ `2 _ : : : _ `n, we build a proof term of the form lemma(p; `1 _ `2 _ : : : _ `n), where p is constructed by examining the justifications for :`1; : : : ; :`n. If :`i is a decision literal, then the justification for :`i is a term hypothesis(:`i). If :`i was inferred by unit propagation (so there is a fact :`i in M, with justification C _ :`i), then it is proved using unit-resolution and the justification for the clause C _ :`i.

We see that this approach does not require logging resolution steps for every unit-propagation, but delays the analysis of which unit propagation steps are useful until conflict resolution. The approach also does not produce a resolution proof directly. It produces a natural deduction style proof with hypotheses.

Other propositional rules that are used during proof-reconstruction are: asserted(j) The formula j is a user-supplied assumption. goal(j) The formula j is a user-supplied goal. A goal is symmetric to asserted, but allows retaining the distinction between goals and assumptions in proof objects. mp(p; q; j) Proof of j by modus ponens. Assume that con(p) = y and that con(q) is either y ! j or y $ j. The latter form is used extensively in the simplifier to apply equivalence-preserving simplification steps. 3.4.2

Congruence Proofs

In Z3, the congruence closure implementation is tightly integrated with the Boolean satisfiability core. It serves as a main hub for equality propagation. The efficient extraction of minimal justifications for congruence closure proofs has been studied extensively, [ 11 ]. We here summarize the proof objects that are extracted from the justifications.

The theory of equality can be captured by axioms for reflexivity, symmetry, transitivity, and substitutivity of equality. We encode these axioms as inference rules, and furthermore only specify that these inference rules apply for any binary relation that is reflexive, symmetric, transitive, and/or reflexivemonotone. We use the terminology, reflexive-monotone, for relations that are reflexive and monotone in a given function symbol f . In particular, the relation (from Section 2.1) is also an equivalence relation, and reflexive-monotone over conjunction and disjunction. So the rules are: refl(R(t;t)) A proof for R(t;t), where R is a reflexive relation. symm(p; R(t; s)) A proof of R(t; s), where R is a symmetric relation, and con(p) = R(s;t). trans(p; q; R(t; s)) A proof of R(t; s), where R is transitive, and con(p) = R(t; u) and con(q) = R(u; s). monotonicity(p1; ::; pn; R( f (t1; ::; tn); f (s1; ::; sn))) A proof of R( f (t1; ::; tn); f (s1; ::; sn)), where con(p1) = R(t1; s1), : : : ; con(pn) = R(tn; sn), and R is reflexive and monotone in f . The antecedent pi can be suppressed if ti = si. That is, reflexivity proofs are suppressed to save space.

Our congruence closure core maintains a congruence table. A congruence table enables propagation of equalities over function symbols, so that for example if f (s;t) is a term, and s0 is equal to s, then when creating f (s0;t) it is detected that the potentially new term is in the same congruence class as f (s;t). The implementation also treats equality as a function, and every equality is also inserted to the congruence table. This makes detecting implied dis-equalities simple: given two terms s and t, search the congruence table for an existing entry for s ' t. If the table contains such a literal, then check if the literal is assigned to false. To make this use of the congruence table effective it understands commutative operations, such as equality. This implicit use of commutativity gets reflected in the generated proof terms, and we include a special rule for commutative functions. It can be instantiated for equalities. comm( f (s;t) ' f (t; s)), comm( f (s;t) $ f (t; s)) where f is a commutative function (relation). 3.4.3

Theory lemmas

In the DPLL(T ) architecture, decision procedures for a theory T identify sets of asserted T -inconsistent literals. Dually, the disjunction of the negated literals are T -tautologies. Consequently, proof terms created by theories can be summarized using a single form, here called Theory lemmas. th lemma(p1; : : : ; pn; j) Generic proof rule for theory lemmas. The formula con(p1) ^ : : : ^ con(pn) ! j should be a T -tautology. 3.5

Applications

Z3 with proofs is still under development and has not been released yet. An obvious current application is that proofs offer a simple litmus test on the implementation for soundness bugs. We integrate a simple, but partial (it does not check T -lemmas) proof-checker in Z3 for this purpose. A much more effective strategy for debugging bugs in theory solvers has been to dump the T -lemmas as they are produced. Similar to [ 20 ], we can then apply an independent solver (namely, our previous version of Z3) on the T -lemmas. We found this approach very effective in debugging optimizations that turned out to be unsound.

We also have a facility for displaying proof-terms, but the proof term visualization very easily becomes too large to be of any use.

In future applications, we envision applications of proofs in Z3, such as: Proof-mining [ 17 ]; can proofs be mined for strategies that are helpful for speeding up proofs for a class of problems? Interpolation. Proof visualization. Finally, in the context of Isabelle/HOL, it has been suggested [ 8 ] to translate HOL formulas (which use polymorphism), into first-order untyped formulas. A potentially unsound translation is then run through first-order provers, but the produced proofs (currently apparently only Prover9), can be checked for whether they use inferences that contradict the types. 3.6

The overhead of enabling proofs

We benchmarked proof generation on a few selected, but non-trivial examples from SMT-LIB. The samples show a memory overhead of between 3x-40x, and corresponding slowdowns of 1.1x to 3x. Benchmark NEQ016 size7 PEQ010 size8 fischer6-mutex-14 cache.inv16 xs 20 40

Without Proofs 26.01 secs 9.1 MB 6.65 secs 9.3 MB 7.01 secs 14 MB 15.99 secs 11 MB 2.2 secs 5.8 MB

Models

We will very briefly summarize the model generation features in Z3. More material is available on-line on http://research.microsoft.com/projects/z3/models.html.

Z3 has the ability to produce models as part of its output. Models assign values to the constants in the input and generate finite or partial function graphs for predicates and function symbols.

A model comprises of a set of partitions, each partition is printed as: *k, where k is a non-negative number. Each partition is associated with a set of constants from the input, and is associated with a concrete value. A concrete value can be either a Boolean (true or false), a numeral (with type Int, Real, or BitVec[n]), an array (represented as a finite map), a tuple (represented by a constructor and sequence of values for the fields), or an an uninterpreted ur-element. Ur-elements are internally represented as natural number numerals, but with an uninterpreted type.

By default Z3, produces a full (and compact) interpretation for free functions. There is an option to force Z3 to not assign interpretations to functions when their values don’t influence the truth assignment to the formula.

Z3 version 2 integrates a superposition theorem prover [ 4 ]. When it is able to finitely saturate the set of non-ground input clauses, it can also report that the non-ground formula that was provided is satisfiable, but there are no other mechanisms for extracting additional information from the saturated set of clauses. 4.1

Applications

Models are by now used in a number of Z3 clients. The main clients that use models are the program exploration and test-case generation tools Pex and SAGE (we refer to [ 3 ] for all pointers). They extract symbolic path conditions by monitoring program executions and use Z3 to find alternate inputs that can guide the next execution into a different branch. Models are also used for improved debugging feedback from Spec# and for iterative counter-example guided refinement in the context of bounded model checking of model programs.

We also believe that the availability of models can in future applications play a useful role in the context of model-based quantifier instantiation and integrating external decision procedures with Z3. 5

Conclusions

We presented the proof and model generation facilities in Z3. Models have already shown particular usefulness in the context of SMT applications. Proofs will be available in Z3 v2, and we hope, in light of this introduction, that users will be able to find useful applications of the feature.

References

[1] Aaron Stump and Duckki Oe . Towards an SMT Proof Format . In 6'th International Workshop on SMT, 2008 .

[2] Alessandro Cimatti , Alberto Griggio, and Roberto Sebastiani . Efficient Interpolant Generation in Satisfiability Modulo Theories . In Ramakrishnan and Rehof [15] , pages 397 - 412 .

[3] Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver . In Ramakrishnan and Rehof [ 15 ].

[4] Leonardo de Moura and Nikolaj Bjørner . Engineering DPLL(T) + Saturation . In IJCAR' 08 , 2008 .

[5] Bruno Dutertre and Leonardo de Moura. A Fast Linear-Arithmetic Solver for DPLL(T) . In CAV'06, LNCS 4144 , pages 81 - 94 . Springer-Verlag, 2006 .

[6] Niklas Ee ´n and Niklas So¨rensson. An Extensible SAT-solver . In Enrico Giunchiglia and Armando Tacchella , editors, SAT , volume 2919 of Lecture Notes in Computer Science, pages 502 - 518 . Springer, 2003 .

[7] Imre Lakatos . Proofs and Refutations . Cambridge University Press, 1976 .

[8] Jia Meng and Lawrence C. Paulson. Translating Higher-Order Clauses to First-Order Clauses . J. Autom. Reasoning , 40 ( 1 ): 35 - 60 , 2008 .

[9] Michal Moskal . Rocket-Fast Proof Checking for SMT Solvers . In Ramakrishnan and Rehof [15] , pages 486 - 500 .

[10] Matthew W. Moskewicz , Conor F. Madigan, Ying Zhao , Lintao Zhang , and Sharad Malik . Chaff: Engineering an efficient sat solver . In DAC , pages 530 - 535 . ACM, 2001 .

[11] Robert Nieuwenhuis and Albert Oliveras . Proof-Producing Congruence Closure . In Ju¨rgen Giesl, editor, RTA , volume 3467 of Lecture Notes in Computer Science, pages 453 - 468 . Springer, 2005 .

[12] Robert Nieuwenhuis and Albert Rubio . Paramodulation-Based Theorem Proving . In Robinson and Voronkov [16] , pages 371 - 443 .

[13] Roberto Niewenhuis , Albert Oliveras , and Cesare Tinelli . Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T) . Journal of the ACM , 53 ( 6 ): 937 - 977 , November 2006 .

[14] Andreas Nonnengart and Christoph Weidenbach . Computing small clause normal forms . In Robinson and Voronkov [16] , pages 335 - 367 .

[15] C. R. Ramakrishnan and Jakob Rehof, editors. 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 .

[16] John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes) . Elsevier and MIT Press, 2001 .

[17] S. Schulz . Learning Search Control Knowledge for Equational Theorem Proving . In F. Baader, G. Brewka, and T. Eiter, editors, Proc. of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001) , volume 2174 of LNAI , pages 320 - 334 . Springer, 2001 .

[18] Aaron Stump , Clark W. Barrett, and David L. Dill . Producing proofs from an arithmetic decision procedure in elliptical lf . Electr. Notes Theor. Comput. Sci. , 70 ( 2 ), 2002 .

[19] Aaron Stump and David L. Dill . Faster Proof Checking in the Edinburgh Logical Framework . In Andrei Voronkov, editor, CADE , volume 2392 of Lecture Notes in Computer Science, pages 392 - 407 . Springer, 2002 .

[20] Geoff Sutcliffe. Semantic Derivation Verification: Techniques and Implementation . International Journal on Artificial Intelligence Tools , 15 ( 6 ): 1053 - 1070 , 2006 .

[21] Tjark Weber and Hasan Amjad . Efficiently checking propositional refutations in HOL theorem provers . Journal of Applied Logic , July 2007 .

[22] Yeting Ge and Clark Barrett . Proof Translation and SMT-LIB Benchmark Certification: A Preliminary Report . In 6'th International Workshop on SMT, 2008 .