Haniel Barbosa
email: haniel.barbosa@loria.fr

Jasmin Christian Blanchette
email: jasmin.blanchette@loria.fr

Pascal Fontaine
email: pascal.fontaine@loria.fr

Scalable Fine-Grained Proofs for Formula Processing

We present a framework for processing formulas in automatic theorem provers, with generation of detailed proofs. The main components are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, skolemization, theory-specific simplifications, and expansion of 'let' expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead, and proofs can be checked in linear time. We implemented the approach in the SMT solver veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced, which is important for independent checking and reconstruction in proof assistants.

Introduction

An increasing number of automatic theorem provers can generate certificates, or proofs, that justify the formulas they derive. These proofs can be checked by other programs and shared across reasoning systems. Some users will also want to inspect this output to understand why a formula holds. Proof production is generally well understood for the core proving methods and for many theories commonly used in satisfiability modulo theories (SMT). But most automatic provers also perform some formula processing or preprocessing-such as clausification and rewriting with theory-specific lemmas-and proof production for this aspect is less mature.

For most provers, the code for processing formulas is lengthy and deals with a multitude of cases, some of which are rarely executed. Although it is crucial for efficiency, this code tends to be given much less attention than other aspects of provers. Developers are reluctant to invest effort in producing detailed proofs for such processing, since this requires adapting a lot of code. As a result, the granularity of inferences for formula processing is often coarse. Sometimes, processing features are even disabled to avoid gaps in proofs, at a high cost in proof search performance.

Fine-grained proofs are important for a variety of applications. We propose a framework to generate such proofs without slowing down proof search. Proofs are expressed using an extensible set of inference rules (Sect. 2). The succedent of a rule is an equality between the original term and the translated term. (It is convenient to consider formulas a special case of terms.) The rules have a fine granularity, making it possible to cleanly separate theories. Clausification, theory-specific simplifications, and expansion of 'let' expressions are instances of this framework. Skolemization may seem problematic, but with the help of Hilbert's choice operator, it can also be integrated into the framework. Some provers provide very detailed proofs for parts of the solving, but we are not aware of any publications about practical attempts to provide easily reconstructible proofs for processing formulas containing quantifiers and 'let' expressions.

At the heart of the framework lies a generic contextual recursion algorithm that traverses the terms to translate (Sect. 3). The context fixes some variables, maintains a substitution, and keeps track of polarities or other data. The transformation-specific work, including the generation of proofs, is performed by plugin functions that are given as parameters to the framework. The recursion algorithm, which is critical for the performance and correctness of the generated proofs, needs to be implemented only once. Another benefit of the modular architecture is that we can easily combine several transformations in a single pass, without complicating the code unduly or compromising the level of detail of the proof output. For very large inputs, this can improve performance.

The inference rules and the contextual recursion algorithm enjoy many desirable properties (Sect. 4). The rules are sound, and the treatment of binders is correct even in the presence of name clashes. Moreover, with suitable data structures, proof generation adds an overhead that is proportional to the time spent processing the terms. Checking proofs represented as directed acyclic graphs (DAGs) can be performed with a time complexity that is linear in their size. Detailed proofs of the metatheory are included in a technical report [START_REF] Barbosa | Tech. report associated with this paper[END_REF], together with more explanations and examples.

We implemented the approach in veriT (Sect. 5), an SMT solver that is competitive on problems combining equality, linear arithmetic, and quantifiers [START_REF] Barbosa | Congruence closure with free variables[END_REF]. Compared with other SMT solvers, veriT is known for its very detailed proofs [START_REF] Besson | A flexible proof format for SMT: A proposal[END_REF], which are reconstructed in the proof assistants Coq [START_REF] Armand | A modular integration of SAT/SMT solvers to Coq through proof witnesses[END_REF] and Isabelle/HOL [START_REF] Blanchette | Semi-intelligible Isar proofs from machine-generated proofs[END_REF] and in the GAPT system [START_REF] Ebner | System description: GAPT 2.0[END_REF]. As a proof of concept, we implemented a prototype checker in Isabelle/HOL.

By adopting the new framework, we were able to remove large amounts of complicated code in the solver, while enabling detailed proofs for more transformations than before. The contextual recursion algorithm had to be implemented only once and is more thoroughly tested than any of the monolithic transformations it subsumes. Our empirical evaluation reveals that veriT is as fast as before even though it now generates finer-grained proofs.

Conventions Our setting is a many-sorted classical first-order logic as defined by the SMT-LIB standard [START_REF] Barrett | The SMT-LIB standard: Version 2.5[END_REF]. A signature Σ = (S , F ) consists of a set S of sorts and a set F of function symbols. Nullary function symbols are called constants. We assume that the signature contains a Bool sort and constants true, false : Bool, a family ( : σ × σ → Bool) σ∈S of function symbols interpreted as equality, and the connectives ¬, ∧, ∨, and -→. Formulas are terms of type Bool, and equivalence is equality ( ) on Bool. Terms are built over symbols from F and variables from a fixed family of infinite sets (V σ ) σ∈S .

In addition to ∀ and ∃, we rely on two more binders: Hilbert's choice operator εx. ϕ and a 'let' construct, let xn sn in t, which simultaneously assigns n variables.

We use the symbol = for syntactic equality on terms. We reserve the names a, f, p, q for function symbols; x, y for variables; r, s, t, u for terms (which may be formulas); ϕ, ψ for formulas; and Q for quantifiers (∀ and ∃). We use the notations ān and (a i ) n i=1 to denote the tuple, or vector, (a 1 , . . . , a n ). We write [n] for {1, . . . , n}.

Given a term t, the set of its free variables is written FV(t). The notation t[ xn ] stands for a term that may depend on xn ; t[ sn ] is the corresponding term where the terms sn are substituted for xn . Bound variables in t are renamed to avoid capture. Following these conventions, Hilbert choice and 'let' are characterized by

|= ∃x. ϕ[x] -→ ϕ[εx. ϕ] (ε 1 ) |= (∀x. ϕ ψ) -→ (εx. ϕ) (εx. ψ) (ε 2 ) |= (let
Γ s t Γ t u TRANS if Γ(t) = t Γ s u Γ t i u i n i=1 CONG Γ f( tn ) f(ū n ) Γ, y, x → y ϕ ψ BIND if y / ∈ FV(Qx. ϕ) Γ (Qx. ϕ) (Qy. ψ) Γ, x → (εx. ϕ) ϕ ψ SKO ∃ Γ (∃x. ϕ) ψ Γ, x → (εx. ¬ ϕ) ϕ ψ SKO ∀ Γ (∀x. ϕ) ψ Γ r i s i n i=1 Γ, xn → sn t u LET if Γ(s i ) = s i for all i ∈ [n] Γ (let xn rn in t) u
• TAUT T relies on an oracle |= T to derive arbitrary lemmas in a theory T . In practice, the oracle will produce some kind of certificate to justify the inference. An important special case, for which we use the name REFL, is syntactic equality.

• TRANS needs the side condition because the term t appears both on the left-hand side of (where it is subject to Γ's substitution) and on the right-hand side. • CONG can be used for any function symbol f, including the logical connectives.

• BIND is a congruence rule for quantifiers. The rule also justifies the renaming of the bound variable. The side condition prevents an unwarranted variable capture. In the antecedent, the renaming is expressed by a substitution in the context. • SKO ∃ and SKO ∀ exploit (ε 1 ) to replace a quantified variable with a suitable witness, simulating skolemization. We can think of the ε expression in each rule abstractly as a fresh function symbol that takes any fixed variables it depends on as arguments. • LET exploits (let) to expand a 'let' expression. The terms rn assigned to the variables xn can be transformed into terms sn .

The antecedents of all the rules inspect subterms structurally, without modifying them. Modifications to the term on the left-hand side are delayed; the substitution is applied only in TAUT. This is crucial to obtain compact proofs that can be checked efficiently. By systematically renaming variables in BIND, we can satisfy most side conditions trivially.

Judgments can be encoded into a well-understood theory of binders: the simply typed λ-calculus. This provides a solid basis to reason about them, and to reconstruct proofs expressed in the inference system. We refer to our technical report [START_REF] Barbosa | Tech. report associated with this paper[END_REF] for details.

The set of rules can be extended to cater for arbitrary transformations that can be expressed as equalities, using Hilbert choice to represent fresh symbols if necessary. The usefulness of Hilbert choice for proof reconstruction is well known [START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF][START_REF] De Nivelle | Translation of resolution proofs into short first-order proofs without choice axioms[END_REF][START_REF] Paulson | Source-level proof reconstruction for interactive theorem proving[END_REF], but we push the idea further and use it to simplify the inference system and make it more uniform.

Example 1. The following derivation tree justifies the expansion of a 'let' expression:

CONG a a REFL x → a x a REFL x → a x a CONG x → a p(x, x) p(a, a) LET (let x a in p(x, x)) p(a, a)
Skolemization can be applied regardless of polarity. Normally, we skolemize only positive existential quantifiers and negative universal quantifiers. However, skolemizing other quantifiers is sound in the context of proving. The trouble is that it is generally incomplete, if we introduce Skolem symbols and forget their definitions in terms of Hilbert choice. To paraphrase Orwell, all quantifiers are skolemizable, but some quantifiers are more skolemizable than others.

The output is generated by a proof module that maintains a stack of derivation trees. The procedure apply(R, n, Γ, t, u) pops n derivation trees Dn from the stack and pushes the tree of Γ t u obtained by applying rule R to Dn . The plugin functions are responsible for invoking apply as appropriate.

The Generic Algorithm The algorithm performs a depth-first postorder contextual recursion on the term to process. Subterms are processed first; then an intermediate term is built from the resulting subterms and is processed in turn. The context ∆ is updated in a transformation-specific way with each recursive call. It is abstract from the point of view of the algorithm. The plugin functions are divided into two groups: ctx_let, ctx_quant, and ctx_app update the context when entering the body of a binder or when moving from a function symbol to one of its arguments; build_let, build_quant, build_app, and build_ var return the processed term and produce the corresponding proof as a side effect. function process(∆, t) match t case x: return build_var(∆, x) case f( tn ):

∆ n ← (ctx_app(∆, f, tn , i)) n i=1 return build_app ∆, ∆ n , f, tn , (process(∆ i , t i )) n i=1 case Qx. ϕ: ∆ ← ctx_quant(∆, Q, x, ϕ) return build_quant(∆, ∆ , Q, x, ϕ, process(∆ , ϕ)) case let xn rn in t : ∆ ← ctx_let(∆,
), f(ū n )) return f(ū n ) function ctx_quant(Γ, Q, x, ϕ) y ← fresh variable return Γ, y, x → y function build_quant(Γ, Γ , Q, x, ϕ, ψ) y ← Γ (x) apply(BIND, 1, Γ, Qx. ϕ, Qy. ψ) return Qy. ψ function build_var(Γ, x) apply(REFL, 0, Γ, x, Γ(x)) return Γ(x)
The ctx_let and build_let functions process 'let' expressions. In ctx_let, the substituted terms are processed further before they are added to a substitution entry in the context. In build_let, the LET rule is applied and the transformed term is returned. Analogously, the ctx_quant and build_quant functions rename quantified variables systematically. This ensures that any variables that arise in the range of the substitution specified by ctx_ let will resist capture when the substitution is applied. Finally, the ctx_app, build_app, and build_var functions simply reproduce the term traversal in the generated proof; they perform no transformation-specific work.

Example 2. Following up on Example 1, assume ϕ = let x a in p(x, x). Given the above plugin functions, process(∅, ϕ) returns p(a, a). It is instructive to study the evolution of the stack during the execution of process. First, in ctx_let, the term a is processed recursively; the call to build_app pushes a nullary CONG step with succedent a a onto the stack. Then the term p(x, x) is processed. For each of the two occurrences of x, build_var pushes a REFL step onto the stack. Next, build_app applies a CONG step to justify rewriting under p: The two REFL steps are popped, and a binary CONG is pushed. Finally, build_let performs a LET inference with succedent ϕ p(a, a) to complete the proof: The two CONG steps on the stack are replaced by the LET step. The stack now consists of a single item: the derivation tree of Example 1.

Skolemization Our second transformation, skolemization, assumes that 'let' expressions have been expanded and bound variables have been renamed apart. The context is a pair ∆ = (Γ, p), where Γ is as defined in Sect. 2 and p is the polarity (+, -, or ?) of the term being processed. The main plugin functions are those that manipulate quantifiers:

function ctx_quant((Γ, p), Q, x, ϕ) if (Q, p) ∈ {(∃, +), (∀, -)} then Γ ← Γ, x → sko_term(Γ, Q, x, ϕ) else Γ ← Γ, x return (Γ , p)
The polarity is updated by ctx_app, which is not shown. For example, ctx_app((Γ, -), ¬, ϕ, 1) returns (Γ, +), because if ¬ ϕ occurs negatively in a larger formula, then ϕ occurs positively. The plugin functions build_app and build_var are as for 'let' expansion.

Positive occurrences of ∃ and negative occurrences of ∀ are skolemized. All other quantifiers are kept as they are. The sko_term function returns an applied Skolem function symbol following some reasonable scheme; for example, outer skolemization [START_REF] Nonnengart | Computing small clause normal forms[END_REF] creates an application of a fresh function symbol to all variables fixed in the context. To comply with the inference system, the application of SKO ∃ or SKO ∀ in build_quant instructs the proof module to systematically replace the Skolem term with the corresponding ε term when outputting the proof.

Theory Simplification All kinds of theory simplification can be performed on formulas. We restrict our focus to a simple yet quite characteristic instance: the simplification of u + 0 and 0 + u to u. We assume that 'let' expressions have been expanded. The context is a list of fixed variables. The plugin functions ctx_app and build_var are as for 'let' expansion; the remaining ones are presented below.

function ctx_quant(Γ, Q, x, ϕ) return Γ, x function build_quant(Γ, Γ , Q, x, ϕ, ψ) apply(BIND, 1, Γ, Qx. ϕ, Qx. ψ) return Qx. ψ function build_app(Γ, Γ n , f, tn , ūn ) apply(CONG, n, Γ, f( tn ), f(ū n )) if f(ū n ) has form u+0 or 0+u then apply(TAUT + , 0, Γ, f(ū n ), u) apply(TRANS, 2, Γ, f( tn ), u) return u else return f(ū n )
The quantifier manipulation code, in ctx_quant and build_quant, is straightforward. The interesting function is build_app. It first applies the CONG rule to justify rewriting the arguments. Then, if the resulting term f(ū n ) can be simplified further into a term u, it performs a transitive chain of reasoning:

f( tn ) f(ū n ) u.
Combinations of Transformations Theory simplification can be implemented as a family of transformations, each member of which embodies its own set of theory-specific rewrite rules. If the union of the rewrite rule sets is confluent and terminating, a unifying implementation of build_app can apply the rules in any order until a fixpoint is reached. Moreover, since theory simplification modifies terms independently of the context, it is compatible with 'let' expansion and skolemization. This allows us to perform arithmetic simplification in the substituted terms of a 'let' expression in a single pass. The combination of 'let' expansion and skolemization is less straightforward. Consider the formula ϕ = let y ∃x.p(x) in y → y. When processing the subformula ∃x.p(x), we cannot (or at least should not) skolemize the quantifier, because it has no unambiguous polarity; indeed, the variable y occurs both positively and negatively in the 'let' expression's body. We can of course give up and perform two passes: The first pass expands 'let' expressions, and the second pass skolemizes and simplifies terms. There is also a way to perform all the transformations in a single instance of the framework, described in our report [START_REF] Barbosa | Tech. report associated with this paper[END_REF].

Scope and Limitations

Other possible instances of contextual recursion are the clause normal form (CNF) transformation and the elimination of quantifiers using one-point rules. CNF transformation is an instance of rewriting of Boolean formulas and can be justified by a TAUT Bool rule. Tseytin transformation can be supported by representing the introduced constants by the formulas they represent, similarly to our treatment of Skolem terms. One-point rules-e.g., the transformation of ∀x. x a -→ p(x) into p(a)-are similar to 'let' expansion and can be represented in much the same way in our framework.

Some transformations, such as symmetry breaking [START_REF] Déharbe | Exploiting symmetry in SMT problems[END_REF] and rewriting based on global assumptions, require a global analysis of the problem that cannot be captured by local substitution of equals for equals. They are beyond the scope of the framework. Other transformations, such as simplification based on associativity and commutativity of function symbols, require traversing the terms to be simplified when applying the rewriting. Since process visits terms in postorder, the complexity of the simplifications would be quadratic, while a processing that applies depth-first preorder traversal can perform the simplifications with a linear complexity. Hence, applying such transformations optimally is also outside the scope of the framework.

Theoretical Properties

The first two metatheoretical results below concern the soundness of the inference rules and the correctness of the recursion algorithm that generates proofs in that system. The other results have to do with the cost of proof generation and checking.

Theorem 1 (Soundness of Inferences). If judgment Γ t u is derivable using the inference system with theories T 1 , . . . , T n , then

|= T 1 ∪ ••• ∪ T n ∪ ∪ ε ∪ let Γ(t) u.
Theorem 2 (Total Correctness of Recursion). For the instances presented in Sect. 3, the contextual recursion algorithm always produces correct proofs.

Observation 3 (Complexity of Recursion).

For the instances presented in Sect. 3, the 'process' function is called at most once on every subterm of the input.

As a corollary, if all the operations performed in process excluding the recursive calls can be accomplished in constant time, the algorithm has linear-time complexity with respect to the input. There exist data structures for which the following operations take constant time: extending the context with a fixed variable or a substitution, accessing direct subterms of a term, building a term from its direct subterms, choosing a fresh variable, applying a context to a variable, checking if a term matches a simple template, and associating the parameters of the template with the subterms. Thus, it is possible to have a linear-time algorithm for 'let' expansion and simplification. On the other hand, skolemization is at best quadratic in the worst case.

Observation 4 (Overhead of Proof Generation). For the instances presented in Sect.3, the number of 'apply' calls is proportional to the number of subterms in the input.

Notice that all arguments to apply must be computed regardless of the apply calls. If an apply call takes constant time, the proof generation overhead is linear in the size of the input. To achieve this performance, it is necessary to use sharing to represent contexts and terms in the output.

Observation 5 (Cost of Proof Checking). Checking an inference step can be performed in constant time if checking the side condition takes constant time.

The above statement may appear weak, since checking the side conditions might itself be linear, leading to a cost of proof checking that can be at least quadratic in the size of the proof. Fortunately, most of the side conditions can be checked efficiently. For example, simplification proofs can be checked in linear time because subst(Γ) is always the identity. Moreover, certifying a proof by checking each step locally is not the only possibility. An alternative is to use an algorithm similar to the process function to check a proof in the same way as it has been produced, exploiting sophisticated invariants.

Implementation

The ideas presented in this paper have been implemented in two tools. We implemented the contextual recursion algorithm and the transformations described in Sect. 3 in the SMT solver veriT [START_REF] Bouton | veriT: An open, trustable and efficient SMT-solver[END_REF], showing that replacing the previous ad hoc code with the generic proof-producing framework had no significant detrimental impact on the solving times. In addition, we developed a prototypical proof checker for the inference system described in Sect. 2 using Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF], to convince ourselves that veriT's output can easily be reconstructed.

Isabelle The Isabelle/HOL proof assistant is based on classical higher-order logic (HOL), a variant of the simply typed λ-calculus. The proof checker is included in the development version of Isabelle. 1Derivations are represented by a recursive datatype in Standard ML, Isabelle's primary implementation language. A derivation is a tree whose nodes are labeled by rule names. Rule TAUT T also carries a theorem that represents the oracle |= T , and rules TRANS and LET are labeled with the terms that occur only in the antecedent (t and sn ). Judgments Γ t u are translated to HOL equalities t u , where t and u are HOL terms in which the context Γ is encoded using λ-abstractions and (for substitutions) applications. For example, the judgment x, y → g(x) f(y) f(g(x)) is represented by the HOL equality (λx. (λy. f y) (g x)) (λx. f (g x)).

Because reconstruction is not verified, there are no guarantees that it will always succeed, but when it does, the result is certified by Isabelle's LCF-style inference kernel [START_REF] Gordon | Edinburgh LCF: A Mechanised Logic of Computation[END_REF]. We hard-coded a few dozen examples to test different cases, such as this one: Given the HOL terms

t = ¬ ∀x. p ∧ ∃x. ∀x. q x x u = ¬ ∀x. p ∧ ∃x. q (εx. ¬ q x x) (εx. ¬ q x x)
and the ML tree

N (Cong, [N (Bind, [N (Cong, [N (Refl, []), N (Bind, [N (Sko_All, [N (Refl, [])])])])])]))
the reconstruction function returns the HOL theorem t u.

veriT We implemented the contextual recursion framework in the SMT solver veriT,2 replacing large parts of the previous non-proof-producing, hard-to-maintain code. Even though it offers more functionality (proof generation), the preprocessing module is about 20% smaller than before and consists of about 3000 lines of code. There are now only two traversal functions instead of 10. This is, for us, a huge gain in maintainability.

We were able to reuse its existing proof module and proof format [START_REF] Besson | A flexible proof format for SMT: A proposal[END_REF]. A proof is a list of inferences, each of which consists of an identifier, the name of the rule, the identifiers of the dependencies, and the derived clause. The use of identifiers makes it possible to represent proofs as DAGs. We extended the format with the inference rules of Sect. 2. The rules that augment the context take a sequence of inferences-a subproof -as a justification. The subproof occurs within the scope of the extended context.

In contrast with the abstract proof module described in Sect. 3, veriT leaves REFL steps implicit for judgments of the form Γ t t. The other inference rules are generalized to cope with missing REFL judgments. In addition, when printing proofs, the proof module can automatically replace terms in the inferences with some other terms. This is necessary for transformations such as skolemization and 'if-then-else' elimination. We must apply a substitution in the replaced term if the original term contains variables. In veriT, efficient data structures are available to perform this.

The implementation of contextual recursion uses a single global context, augmented before processing a subterm and restored afterwards. The context consists of a set of fixed variables, a substitution, and a polarity. In our setting, the substitution satisfies the side conditions by construction. If the context is empty, the result of processing a subterm is cached. For skolemization, a separate cache is used for each polarity. No caching is attempted under binders.

Invoking process on a term returns the identifier of the inference at the root of its transformation proof in addition to the processed term. These identifiers are threaded through the recursion to connect the proof. The proofs produced by instances of contextual recursion are inserted into the larger resolution proof produced by veriT.

Transformations performing theory simplification were straightforward to port to the new framework: Their build_app functions simply apply rewrite rules until a fixpoint is reached. Porting transformations that interact with binders required special attention in handling the context and producing proofs. Fortunately, most of these aspects are captured by the inference system and the abstract contextual recursion framework, where they can be studied independently of the implementation. Some transformations are performed outside of the framework. Proofs of CNF transformation are expressed using the inference rules of veriT's underlying SAT solver, so that any tool that can reconstruct SAT proofs can also reconstruct these proofs. Simplification based on associativity and commutativity of function symbols is implemented as a dedicated procedure, for efficiency reasons. It currently produces coarse-grained proofs.

To evaluate the impact of the new contextual recursion algorithm and of producing detailed proofs, we compare the performance of different configurations of veriT. Our experimental data is available online. 3 We distinguish three configurations. BASIC only applies transformations for which the old code provided some (coarse-grained) proofs. EXTENDED also applies transformations for which the old code did not provide any proofs, whereas the new code provides detailed proofs. COMPLETE applies all transformations available, regardless of whether they produce proofs.

More specifically, BASIC applies the transformations for 'let' expansion, skolemization, elimination of quantifiers based on one-point rules, elimination of 'if-then-else', theory simplification for rewriting n-ary symbols as binary, and elimination of equivalences and exclusive disjunctions with quantifiers in subterms. EXTENDED adds Boolean and arithmetic simplifications to the transformations performed by BASIC. COMPLETE performs global rewriting simplifications and symmetry breaking in addition to the transformations in EXTENDED.

The evaluation relies on two main sets of benchmarks from SMT-LIB [START_REF] Barrett | The SMT-LIB standard: Version 2.5[END_REF] without bit vectors and nonlinear arithmetic (currently not supported by veriT): the 20 916 benchmarks in the quantifier-free (QF) categories, and the 30 250 benchmarks labeled as unsatisfiable in the non-QF categories. Our experiments were conducted on servers equipped with two Intel Xeon E5-2630 v3 processors, with eight cores per processor, and 126 GB of memory. Each run of the solver uses a single core. The time limit was set to 30 s, a reasonable value for interactive use within a proof assistant. These results indicate that the new generic contextual recursion algorithm and the production of detailed proofs do not impact performance negatively compared with the old code and coarse-grained proofs. Moreover, allowing Boolean and arithmetic simplifications leads to some improvements. We expect that generating proofs for the global transformations would lead to substantial improvements on quantifier-free problems.

Related Work

Most automatic provers that support the TPTP syntax for problems generate proofs in TSTP format [START_REF] Sutcliffe | Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems[END_REF]. Like a veriT proof, a TSTP proof consists of a list of inferences. TSTP does not mandate any inference system; the meaning of the rules and the granularity of inferences vary across systems. For example, the E prover [START_REF] Schulz | System description: E 1.8[END_REF] combines clausification, skolemization, and variable renaming into a single inference, whereas Vampire [START_REF] Kovács | First-order theorem proving and Vampire[END_REF] appears to cleanly separate preprocessing transformations. SPASS's [START_REF] Weidenbach | SPASS version 3.5[END_REF] custom proof format does not record preprocessing steps; reverse engineering is necessary to make sense of its output, and optimizations ought to be disabled [START_REF] Blanchette | Semi-intelligible Isar proofs from machine-generated proofs[END_REF]Sect. 7.3].

Most SMT solvers can parse the SMT-LIB [START_REF] Barrett | The SMT-LIB standard: Version 2.5[END_REF] format, but each solver has its own output syntax. Z3's proofs can be quite detailed [START_REF] De Moura | Proofs and refutations, and Z3[END_REF], but rewriting steps often combine many rewrites rules. CVC4's format is an instance of LF [START_REF] Harper | A framework for defining logics[END_REF] with Side Conditions (LFSC) [START_REF] Stump | Proof checking technology for satisfiability modulo theories[END_REF]; despite recent progress [START_REF] Hadarean | Fine grained SMT proofs for the theory of fixed-width bit-vectors[END_REF][START_REF] Katz | Lazy proofs for dpll(t)-based SMT solvers[END_REF], neither skolemization nor quantifier instantiation are currently recorded in the proofs. Proof production in Fx7 [START_REF] Moskal | Rocket-fast proof checking for SMT solvers[END_REF] is based on an inference system whose formula processing fragment is subsumed by ours; for example, skolemization is more ad hoc, and there is no explicit support for rewriting.

Conclusion

We presented a framework to represent and generate proofs of formula processing and its implementation in veriT and Isabelle/HOL. The framework centralizes the delicate issue of manipulating bound variables and substitutions soundly and efficiently, and it is flexible enough to accommodate many interesting transformations. Although it was implemented in an SMT solver, there appears to be no intrinsic limitation that would prevent its use in other kinds of first-order, or even higher-order, automatic provers. The framework covers many preprocessing techniques and can be part of a larger toolbox.

Detailed proofs have been a defining feature of veriT for many years now. It now produces more detailed justifications than ever, but there are still some global transformations for which the proofs are nonexistent or leave much to be desired. In particular, supporting rewriting based on global assumptions would be essential for proof-producing inprocessing, and symmetry breaking would be interesting in its own right.

  xn sn in t[ xn ]) t[ sn ] (let)Substitutions ρ are functions from variables to terms such that ρ(x i ) = x i for at most finitely many variables x i . We write them as { xn → sn }. The substitution ρ[ xn → sn ] maps each variable x i to the term s i and otherwise coincides with ρ. The application of a substitution ρ to a term t is denoted by ρ(t). It is capture-avoiding; bound variables in t are renamed as necessary. Composition ρ • ρ is defined as for functions (i.e., ρ is applied first).The inference rules used by our framework depend on a notion of context defined by the grammar Γ ::= ∅ | Γ, x | Γ, xn → sn . Each context entry either fixes a variable x or defines a substitution { xn → sn }. If a context introduces the same variable several times, the rightmost entry shadows the others. Abstractly, a context Γ fixes a set of variables and specifies a substitution subst(Γ) defined by subst(∅) = {}, subst(Γ, x) = subst(Γ)[x → x], and subst(Γ, xn → tn ) = subst(Γ) • { xn → tn }. In the second equation, the [x → x] update shadows any replacement of x induced by Γ. We write Γ(t) to abbreviate the capture-avoiding substitution subst(Γ)(t).Transformations of terms (and formulas) are justified by judgments of the form

	2 Inference System

  The table below shows the number of problems solved in total by each configuration.

		Without proofs	With proofs
		Old code New code Old code New code
	BASIC	42 235	42 258	42 104	42 118
	EXTENDED	42 324	42 389	N/A	42 271
	COMPLETE	42 585	42 613	N/A	N/A

Γ t u, where Γ is a context, t is an unprocessed term, and u is the corresponding processed term. The free variables in t and u must appear in the context Γ. Semantically, the judgment expresses the equality of the terms Γ(t) and u for all variables fixed by Γ. Crucially, the substitution applies only on the left-hand side of the equality.The inference rules for the transformations covered in this paper are presented below.TAUT T if |= T Γ(t) u Γ t u

Contextual RecursionWe propose a generic algorithm for term transformations, based on structural recursion. The algorithm is parameterized by a few simple plugin functions embodying the essence of the transformation. By combining compatible plugin functions, we can perform several transformations in one traversal. Transformations can depend on some context that encapsulates relevant information, such as bound variables, variable substitutions, and polarity. Each transformation can define its own notion of context.

http://isabelle.in.tum.de/repos/isabelle/file/00731700e54f/src/HOL/ex/veriT _ Preprocessing.thy

http://matryoshka.gforge.inria.fr/pubs/processing/veriT.tar.gz

http://matryoshka.gforge.inria.fr/pubs/processing/

https://doi.org/10.5281/zenodo.582482

Acknowledgment We thank Simon Cruanes for discussing many aspects of the framework with us as it was emerging, and we thank Robert Lewis, Stephan Merz, Lawrence Paulson, Anders Schlichtkrull, Mark Summerfield, Sophie Tourret, and the anonymous reviewers for suggesting many textual improvements. This research has been partially supported by the Agence nationale de la recherche / Deutsche Forschungsgemeinschaft project SMArT (ANR-13-IS02-0001, STU 483/2-1) and by the European Union project SC 2 (grant agreement No. 712689). The work has also received funding from the European Research Council under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Experiments presented in this paper were carried out using the Grid'5000 testbed (https://www.grid5000. fr/), supported by a scientific interest group hosted by Inria and including CNRS, RENATER, and several universities as well as other organizations. A mirror of all the software and evaluation data described in this paper is hosted by Zenodo. 4