Sophie Tourret
email: stourret@mpi-inf.mpg.de

Jasmin Blanchette
email: j.c.blanchette@vu.nl

A Modular Isabelle Framework for Verifying Saturation Provers

Keywords: CCS Concepts:, Theory of computation → Logic and verification; Automated reasoning automatic theorem provers, proof assistants, first-order logic

We present a formalization in Isabelle/HOL of a comprehensive framework for proving the completeness of automatic theorem provers based on resolution, superposition, or other saturation calculi. The framework helps calculus designers and prover developers derive, from the completeness of a calculus, the completeness of prover architectures implementing the calculus. It also helps derive the completeness of calculi obtained by lifting ground (i.e., variable-free) calculi. As a case study, we re-verified Bachmair and Ganzinger's resolution prover RP to show the benefits of modularity.

Introduction

Many of the most successful automatic theorem provers today are based on saturation. These include the unit equality prover Waldmeister [START_REF] Hillenbrand | The next Waldmeister loop[END_REF], the first-order provers E [START_REF] Schulz | Faster, higher, stronger: E 2.3[END_REF], SPASS [START_REF] Weidenbach | SPASS version 3.5[END_REF], and Vampire [START_REF] Kovács | First-order theorem proving and Vampire[END_REF], and the higher-order provers Leo-III [START_REF] Steen | The higher-order prover Leo-III[END_REF] and Zipperposition [START_REF] Bentkamp | Superposition with lambdas[END_REF]. A saturation prover starts with a problem, typically given in conjunctive normal form, and draws inferences from the problem clauses, adding the conclusions to the clause set. If the prover detects useless clauses, it may remove them. A refutation proof has been found when the prover has derived the empty clause, denoted by ⊥. Which inferences are drawn and which clauses are deemed redundant depends on the logical calculus used.

Although users mostly care only about the soundness and success rate of a prover, refutational completeness is taken very seriously by researchers. Beyond its intrinsic merits, completeness is useful to optimize a calculus: From a completeness proof, calculi designers can extract precise side conditions on the inference rules, which help prune the search space. Without the guidance offered by a completeness proof, it is easy to prune too little, too much, or both. Moreover, for decidable fragments, completeness is needed to ensure that the prover can be relied on as a decision procedure.

Completeness can be formulated in two ways:

• Static completeness is stated in terms of a "saturated" clause set N -a set from which all necessary inferences have been drawn.

• Dynamic completeness is stated in terms of a sequence (N i ) i of clause sets, where each set N i represents the prover's state at a point in time: If N 0 is unsatisfiable (i.e., the conjecture holds), then ⊥ ∈ N i for some i.

Most saturation calculi are designed as a lifting of a ground calculus-that is, a calculus that operates on variable-free clauses. Static completeness is established on the ground level and lifted along with the calculus. This separation of concerns helps keep these technical proofs manageable.

For dynamic completeness, we distinguish between simple proving processes that operate on a single clause set and realistic provers with multiple clause sets. The given clause procedure [17, Section 2.3], which is part of virtually all saturation provers, needs two clause sets, called "passive" and "active." Clauses are initially passive and move one by one to the active set, at which point all possible inferences with active partners are drawn. This setup is reminiscent of traditional New Year celebrations in Quebec: When you arrive at the party, you must kiss all the relatives lined up before you and then join the line. In this way, everybody kisses everybody.

A crucial optimization in provers is clause subsumption. A clause D, seen as a multiset of literals, subsumes another clause C if Dσ ⊆ C for some substitution σ ; for example, p(x) subsumes p(a) and p(x) ∨ q(y). Regrettably, much of the literature on saturation ignores subsumption and dynamic completeness. In the refinement chain leading to a verified prover, such a simplifying assumption translates into a proof gap.

Bachmair and Ganzinger's chapter in the Handbook of Automated Reasoning [START_REF] Bachmair | Resolution theorem proving[END_REF] is an exception. They define a threeclause-set resolution prover, called RP, that supports clause subsumption, and they prove it dynamically complete. But their argument is highly nonmodular: They move directly from static completeness of the ground calculus to dynamic completeness of RP, awkwardly mixing issues related to nonground lifting, subsumption, and the given clause procedure. The argument is hard to follow on paper, and even harder to formalize, as Schlichtkrull, Blanchette, Traytel, and Waldmann found out [START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's ordered resolution prover[END_REF].

To remedy this situation, Waldmann, Tourret, Robillard, and Blanchette [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF] designed a comprehensive framework that covers a wide range of calculi, including ordered resolution [START_REF] Bachmair | Resolution theorem proving[END_REF], unfailing completion [START_REF] Bachmair | Completion without failure[END_REF], standard superposition [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF], constraint superposition [START_REF] Nieuwenhuis | Theorem proving with ordering and equality constrained clauses[END_REF], theory superposition [START_REF] Waldmann | Cancellative abelian monoids and related structures in refutational theorem proving (part I)[END_REF], hierarchic superposition [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF], λ-free superposition [START_REF] Bentkamp | Superposition for lambda-free higher-order logic[END_REF], λ-superposition [START_REF] Bentkamp | Superposition with lambdas[END_REF], and combinatory superposition [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF]. This saturation framework can be used to lift ground static completeness to nonground static completeness and then to dynamic completeness of minimalistic proving processes or given clause provers with support for clause subsumption.

The framework was initially developed in L A T E X, but we also managed to formalize it in Isabelle/HOL in time to mention it in Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]Section 5]. The present paper aims at introducing this work to the interactive theorem proving community. Besides giving a thorough account of the formalization, we unveil three extensions of the framework:

• We applied the formalized framework to re-prove RP dynamically complete. The new proof is substantially simpler and shorter than that by Schlichtkrull et al. • We formalized various basic concepts related to theorem proving that were needed to verify RP and that will likely be useful for other provers. Much of this material was generalized from Schlichtkrull et al. • We formalized alternative, invariance-based completeness proofs for given clause procedures. These new proofs replace previous monolithic arguments and will be used, in pen-and-paper form, in a forthcoming journal submission by Waldmann et al.

We used the declarative Isar [START_REF] Wenzel | Isabelle/Isar-a generic framework for human-readable proof documents[END_REF] in the hope that practitioners who are not Isabelle experts can follow the intermediate proof steps. We also relied extensively on locales [START_REF] Ballarin | Locales: A module system for mathematical theories[END_REF], which provide parameterized modules. The vast majority of the pen-and-paper arguments survived formalization, but one serious issue was discovered and repaired.

Our work is part of the IsaFoL (Isabelle Formalization of Logic) effort, an unfunded coalition of the willing that aims at developing a library of results about logic and automated reasoning [START_REF] Christian | Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)[END_REF]. The Isabelle theory files amount to around 5700 lines of source text. They were developed using Isabelle version 2020 and are available in the Archive of Formal Proofs [START_REF] Blanchette | Extensions to the comprehensive framework for saturation theorem proving[END_REF][START_REF] Tourret | A comprehensive framework for saturation theorem proving[END_REF]. The AFP is continuously updated to track Isabelle's evolution, ensuring the compatibility of our theories with the current version of Isabelle. 1This paper's organization largely follows Waldmann et al. Briefly, we introduce the fundamental notions that make up a calculus and related concepts such as saturation and completeness (Section 2); we cover the lifting from the ground to the nonground level and the delicate issue of clause subsumption (Section 3); we present two given clause procedures and our alternative, invariance-based proofs (Section 4); and we present our modular proof of RP's completeness (Section 5).

Calculi

The saturation framework relies on a number of basic notions that are relevant to prove a calculus complete. These include formulas, consequence relations, inference systems, and redundancy criteria (all defined in Calculus.thy, unless indicated otherwise).

Formulas

The entire framework is built on an abstract notion of formulas, generalizing clauses. Formulas are represented by a type variable ′ f equipped with a set Bot and an entailment relation | =. Bot is a nonempty set of patently false formulas. Typically, we take Bot = {⊥}, but it can be useful to differentiate between an active ⊥ and a passive ⊥. Entailment must satisfy four basic properties. Formally:

locale consequence_relation = fixes Bot :: ′ f set and | = :: ′ f set ⇒ ′ f set ⇒ bool assumes Bot ∅ and B ∈ Bot = ■ ⇒ {B} | = N 1 and N 2 ⊆ N 1 = ■ ⇒ N 1 | = N 2 and (∀C ∈ N 2 . N 1 | = {C}) = ■ ⇒ N 1 | = N 2 and N 1 | = N 2 = ■ ⇒ N 2 | = N 3 = ■ ⇒ N 1 | = N 3
An Isabelle locale can be seen as a record type, where fields can be types ( ′ f ), terms (Bot, | =), or properties. When we later instantiate the locale, we must supply concrete arguments for the types and terms and then discharge the proof obligations corresponding to the properties. Locales are invaluable; they allow us to declare parameters and assumptions once and reuse them in multiple related definitions and lemmas. They also emphasize the modular nature of the proof development.

Inference Systems

An inference C n , . . . , C 1 ⊢ C 0 is a recipe to derive a new formula C 0 (the conclusion) from existing formulas C n , . . . , C 1 (the premises). Formally:

datatype ′ f inference = Infer ( ′ f list) ′ f An inference ι is written out as ι = Infer [C n , . . . , C 1 ] C 0 , with prems_of ι = [C n , . . . , C 1 ] and concl_of ι = C 0 .
An inference rule, with its metavariables and side conditions, generally corresponds to a set of inferences. In fact, an entire inference system, consisting of one or more inference rules, is modeled as a set of inferences Inf. Formally:

locale inference_system = fixes Inf :: ′ f inference set
Inside the locale, we defined the following functions:

definition Inf_from :: ′ f set ⇒ ′ f inference set where Inf_from N = {ι ∈ Inf. prems_of ι ⊆ N } definition Inf_between :: ′ f set ⇒ ′ f set ⇒ ′ f inference set where Inf_between N M = Inf_from (N ∪ M) -Inf_from (N -M)
The auxiliary function Inf_from N returns the set of possible inferences from premises contained in N . The variant Inf_ between N M returns the set of possible inferences from premises in N ∪ M but with at least one premise in M.

Calculi with Redundancy

A calculus is basically an inference system equipped with a redundancy criterion. The inference system indicates which inferences must a priori be drawn. The redundancy criterion specifies inferences that can a posteriori be omitted. It also identifies deletable formulas. Formally:

locale calculus = inference_system Inf + consequence_relation Bot (| =) + fixes Red I :: ′ f set ⇒ ′ f inference set and Red F :: ′ f set ⇒ ′ f set assumes Red I N ⊆ Inf and B ∈ Bot = ■ ⇒ N | = {B} = ■ ⇒ N -Red F N | = {B} and N ⊆ N ′ = ■ ⇒ Red F N ⊆ Red F N ′ and N ⊆ N ′ = ■ ⇒ Red I N ⊆ Red I N ′ and N ′ ⊆ Red F N = ■ ⇒ Red F N ⊆ Red F (N -N ′ ) and N ′ ⊆ Red F N = ■ ⇒ Red I N ⊆ Red I (N -N ′ ) and ι ∈ Inf = ■ ⇒ concl_of ι ∈ N = ■ ⇒ ι ∈ Red I N
The locale inherits Inf (and the auxiliaries Inf_from and Inf_ between) from inference_system as well as Bot and | = from consequence_relation.

An inference ι is redundant if ι ∈ Red I N ; a formula C is redundant if C ∈ Red F N .
The locale assumptions are needed to establish dynamic completeness.

For example, the second assumption ensures that deleting a redundant formula from an unsatisfiable set preserves the set's unsatisfiability.

Static and Dynamic Completeness

Static completeness is useful because it is comparatively convenient to formulate and establish. Dynamic completeness is useful because it directly captures a desired property of proving processes. Under some basic assumptions that are met by well-designed redundancy criteria, the two concepts coincide. Thus, we can establish the static completeness of a calculus and immediately obtain the dynamic completeness of a proving process ▷ based on it. Static completeness is expressed in terms of a single formula set N , which must be saturated. Saturation means that all inferences from N are redundant:

definition saturated :: ′ f set ⇒ bool where saturated N ← → Inf_from N ⊆ Red I N
Completeness means that any unsatisfiable saturated set must contain a patent falsehood (typically, ⊥):

locale statically_complete_calculus = calculus + assumes B ∈ Bot = ■ ⇒ saturated N = ■ ⇒ N | = {B} = ■ ⇒ ∃B ′ ∈ Bot. B ′ ∈ N
We abuse terminology above when we write that a set is "unsatisfiable." Given that we only have a notion of entailment but not of modelhood, it would be more proper (but less standard) to write "inconsistent. "

Dynamic completeness more closely models saturation provers. It is expressed in terms of a finite or infinite sequence of formula sets represented by the codatatype ′ f set llist. A derivation is a sequence where each pair of successive elements satisfies the following relation:

inductive

▷ :: ′ f set ⇒ ′ f set ⇒ bool where M -N ⊆ Red F N = ■ ⇒ M ▷ N
The ▷ relation represents an abstract nondeterministic proving process. Informally, when taking a transition from a set M to another set N , a prover can add arbitrary formulas (corresponding to N -M), and it can remove arbitrary formulas (corresponding to M -N ) as long as these are redundant w.r.t. N . Most provers would add only formulas that are entailed by M, but this is not enforced by ▷.

We write chain (▷) Ns to express that the sequence Ns is a derivation: Above, Liminf Ns denotes the limit inferior i j ≥i Ns ! j, and Sup Ns denotes the supremum i Ns ! i. In accordance with the automated reasoning literature, we will refer to Liminf Ns as the limit of Ns.

Ns ! 0 ▷ Ns ! 1 ▷ • • • ,
Intuitively, a fair derivation is one where every inference with premises in the limit was made redundant at some index i, usually by adding its conclusion to Ns ! i. Using the locale assumptions about redundancy, it is easy to show that the limit of a fair derivation is saturated.

Dynamic completeness is formulated in its own locale:

locale dynamically_complete_calculus = calculus + assumes B ∈ Bot = ■ ⇒ chain (▷) Ns = ■ ⇒ fair Ns = ■ ⇒ Ns ! 0 | = {B} = ■ ⇒ ∃i < llength Ns. ∃B ′ ∈ Bot. B ′ ∈ Ns ! i
Owing to the conditions on redundancy criteria, static and dynamic completeness are equivalent:

sublocale statically_complete_calculus ⊆ dynamically_complete_calculus sublocale dynamically_complete_calculus ⊆ statically_complete_calculus

The above definitions are all based on Waldmann et al., who in turn largely follow Bachmair and Ganzinger but generalize them. The literature is not entirely consistent on notions such as redundancy, saturation, and fairness. The first group of authors studied variations and showed that completeness and "reduced" completeness coincide. We also formalized these proofs (in Calculus_Variations.thy). They make it possible to mix and match results. For example, suppose that a calculus is proved "reducedly" statically complete in the literature. Instead of redoing the proof in a standard, nonreduced setting, we can reuse the reduced proof as is and derive dynamic completeness using the framework.

Intersection of Redundancy Criteria

There are various situations where a prover may need to apply several redundancy criteria in parallel and identify an inference or formula as redundant only if all the criteria agree. This can be incorporated into the framework as a single intersection criterion. One scenario where this is particularly useful is when redundancy is parameterized by a value q :: ′ q that is known only at the limit. The intersection amounts to a universal quantification "for all q ∈ Q, . . . . " Once we know the limit, we can supply the right value for q.

Although this is not always necessary, each redundancy criterion may use its own consequence relation. Thus, we defined a consequence_relation_family locale parameterized by a set Q :: ′ q set and by a Q-indexed family of consequence relations entails q :: ′ q ⇒ ′ f set ⇒ ′ f set ⇒ bool such that each entails q q, for q ∈ Q, qualifies as a consequence relation. The q subscript in the constant name is there to remind us that the family is indexed by the type ′ q. We will encounter this convention again later.

The next step was to define a single relation | = Q as the intersection of the entails q 's:

definition | = Q :: ′ f set ⇒ ′ f set ⇒ bool where N 1 | = Q N 2 ← → ∀q ∈ Q. entails q q N 1 N 2
We proved that | = Q qualifies as a consequence relation. Next, we defined a locale for intersection calculi, which work with the intersection of a Q-indexed family of redundancy criteria. The definitions (in Intersection_Calculus .thy) follow the same pattern as above. The locale follows:

locale intersection_calculus = inference_system Inf + consequence_relation_family Bot Q entails q + fixes Red Iq :: ′ q ⇒ ′ f set ⇒ ′ f inference set and Red Fq :: ′ q ⇒ ′ f set ⇒ ′ f set assumes Q ∅ and ∀q ∈ Q. calculus Bot Inf (entails q q) (Red Iq q) (Red Fq q)
The redundancy criterion is defined as a pair of intersections:

definition Red I :: ′ f set ⇒ ′ f inference set where Red I N = ( q ∈ Q. Red Iq q N ) definition Red F :: ′ f set ⇒ ′ f set where Red F N = ( q ∈ Q. Red Fq q N )
Intersection calculi qualify as calculi with the intersections Red I and Red F as redundancy criterion:

sublocale calculus Bot Inf (| = Q ) Red I Red F
To show that a calculus is statically complete, it suffices to show that for any saturated set N that does not contain a patent falsehood, there exists an index q ∈ Q according to which N is consistent:

lemma stat_ref_comp_from_bot_in_sat: (∀N . saturated Inf Red I N ∧ (∀B ∈ Bot . B N ) -■ → ∃B ∈ Bot. ∃q ∈ Q. ¬ entails q q N {B}) = ■ ⇒ statically_complete_calculus Bot Inf (| = Q ) Red I Red F 2.6 Soundness An inference system Inf is sound w.r.t. a consequence relation | = if every inference ι ∈ Inf is sound-that is, prems_of ι | = {concl_of ι}.
Soundness can be shown one inference rule at a time, without a sophisticated framework. Nevertheless, we formalized a few basic soundness results, as a convenience to users of the framework (in Soundness.thy).

The main soundness lemma, generalized from Schlichtkrull et al., states that the limit of a sound derivation is unsatisfiable if and only if the initial formula set is unsatisfiable:

lemma unsat_limit_iff : chain (▷) Ns = ■ ⇒ chain (| =) Ns = ■ ⇒ (Liminf Ns | = Bot ← → Ns ! 0 | = Bot)
For the forward direction, the proof by Schlichtkrull et al., like the one by Bachmair and Ganzinger on which it is based, requires compactness-the property that whenever N | = Bot, there exists a finite set M ⊆ N such that M | = Bot. Informally, the argument is as follows: If the limit of Ns is unsatisfiable, by compactness there exists an unsatisfiable finite subset; by the definition of limit, it takes only finitely many steps to reach a set that includes this finite subset. By transitivity of | =, the initial state Ns ! 0 is unsatisfiable.

In a private communication, Waldmann supplied an almost as simple proof that dispenses with compactness. By formalizing this proof, we were able to eliminate a few bureaucratic locales and locale instantiations.

Standard Redundancy

Ground versions of resolution and superposition are parameterized by a well-order < that is lifted to clauses. The completeness proof is a well-founded induction over the elements of a saturated clause set N ⊥ w.r.t. <. Each clause is shown in turn to be true in a candidate model. Such inference systems are called counterexample-reducing. This terminology stems from an alternative formulation of induction as a proof by contradiction starting with the assumption that a minimal counterexample exists [START_REF] Bachmair | Resolution theorem proving[END_REF]Section 4.2].

Counterexample-reducing calculi distinguish between the rightmost, or main, premise and the remaining side premises.

Given an inference

ι = Infer [C n , . . . , C 1 ] C 0 , we have main_ prem_of ι = C 1 and side_prems_of ι = [C n , . . . , C 2 ].
An inference system Inf operating on formulas equipped with a well-order < is counterexample-reducing if the following locale requirements can be met:

fixes I_of :: ′ f set ⇒ ′ f set assumes N ∩ Bot = ∅ = ■ ⇒ D ∈ N = ■ ⇒ I_of N ̸ | = {D} = ■ ⇒ ( C. C ∈ N = ■ ⇒ I_of N ̸ | = {C} = ■ ⇒ D ≤ C) = ■ ⇒ ∃ι ∈ Inf. prems_of ι [] ∧ main_prem_of ι = D ∧ side_prems_of ι ⊆ N ∧ I_of N | = side_prems_of ι ∧ I_of N ̸ | = concl_of ι ∧ concl_of ι < D
Since the framework provides no notion of interpretations, we represent an interpretation as a formula set M and write M | = N to mean "M is a model of N ." Given a formula set, the I_of operator yields a candidate model. The locale assumption states that if N contains no patent falsehoods and D is a minimal counterexample formula in N , then there exists an inference from N that produces an even smaller counterexample.

It is not hard to do nonsensical things using a proof assistant. Adversarial users might define I_of N as {⊥} and use this to show that any calculus is counterexample-reducing. This would not take them very far, however, because they could never connect that definition of I_of with a concrete notion of model suitable for their logic.

Counterexample-reducing inference systems are compatible with the standard redundancy criterion, defined as follows (in Standard_Redundancy_Criterion.thy):

definition Red I :: ′ f set ⇒ ′ f inference set where Red I N = {ι ∈ Inf. ∃M ⊆ N . M ∪ side_prems_of ι | = {concl_of ι} ∧ ∀D ∈ M. D < main_prem_of ι} definition Red F :: ′ f set ⇒ ′ f set where Red F N = {C. ∃M ⊆ N . M | = {C} ∧ ∀D ∈ M. D < C}
For inference systems Inf that reduce counterexamples, we obtain a completeness theorem: If N is saturated w.r.t. the standard redundancy criterion and does not contain a patent falsehood, then I_of N is a model of N .

Clauses

Most As a sanity check and as a convenience to users, we specialized various framework concepts to clauses (in Clausal_ Calculus.thy). In particular, we proved that entailment of ground clauses is compact and tailored the notion of counterexample-reducing inference system as follows:

fixes J_of ::

′ a clause set ⇒ ′ a set assumes ⊥ N = ■ ⇒ D ∈ N = ■ ⇒ ¬ J_of N | = D = ■ ⇒ ( C. C ∈ N = ■ ⇒ ¬ J_of N | = C = ■ ⇒ D ≤ C) = ■ ⇒ ∃ι ∈ Inf. prems_of ι [] ∧ main_prem_of ι = D ∧ side_prems_of ι ⊆ N ∧ J_of N | = side_prems_of ι ∧ ¬ J_of N | = concl_of ι ∧ concl_of ι < D
For this locale, we were able to represent a candidate model more conventionally as a set of true atoms and to use the modelhood relation

| = instead of entailment | = of clauses.
We connected the two formulations of counterexample reduction as a convenience for end users. The abstract locale was instantiated by taking

I_of N = {{if A ∈ J_of N then Pos A else Neg A} | A :: ′ a}
We retrieved the following completeness theorem tuned for clauses:

saturated N = ■ ⇒ ⊥ N = ■ ⇒ J_of N | = N .

Lifting Ground Calculi

The saturation framework supports a variety of approaches to lift ground calculi to the nonground level (in Lifting_ to_Non_Ground_Calculi.thy and Labeled_Lifting_to_ Non_Ground_Calculi.thy). We start with the folklore approach and introduce features incrementally until the result is flexible enough to support the calculi of realistic provers.

Standard Lifting

The standard lifting is based on a pair of grounding functions G F and G I that link nonground formulas (of some type ′ f ) to sets of ground formulas (of some type ′ д) and similarly for nonground and ground inferences. Using these functions, it connects a nonground inference system to a ground calculus:

locale standard_lifting = inference_system Inf F + calculus Bot G Inf G (| =) Red IG Red FG + fixes Bot F :: ′ f set and G F :: ′ f ⇒ ′ д set and G I :: ′ f inference ⇒ ′ д inference set option assumes Bot F ∅ and B ∈ Bot F = ■ ⇒ G F B ∅ and B ∈ Bot F = ■ ⇒ G F B ⊆ Bot G and G F C ∩ Bot G ∅ -■ → C ∈ Bot F and ι ∈ Inf F = ■ ⇒ G I ι None = ■ ⇒ the (G I ι) ⊆ Red IG (G F (concl_of ι))
An instance of the locale for first-order logic would have G F map the nonground formula p(x) to a Herbrand set such as {p(a), p(b), . . . , p(f(a)), p(f(b)), . . . }. As for G I , it maps a nonground inference ι to either a set of ground inferences (accessible via the) or the special value None, which indicates that ι has no counterpart at the ground level.

Entailment of sets of nonground formulas is defined via grounding: Using these notions, we extended the nonground inference system Inf F with a lifted redundancy criterion to form a nonground calculus:

N 1 | = G N 2 ← → G Fset N 1 | = G Fset N 2 ,
definition Red I ::

′ f set ⇒ ′ f inference set where Red I N = {ι ∈ Inf F . (G I ι None ∧ the (G I ι) ⊆ Red IG (G Fset N )) ∨ (G I ι = None ∧ G F (concl_of ι) ⊆ G Fset N ∪ Red FG (G Fset N ))} definition Red F :: ′ f set ⇒ ′ f set where Red F N = {C. ∀D ∈ G F C. D ∈ Red FG (G Fset N )} sublocale calculus Bot F Inf F (| = G ) Red I Red F
This brings us to our first main result. If the ground calculus is statically complete and overapproximated by the nonground calculus, then the latter is statically complete as well: theorem stat_ref_comp_to_non_ground:

assumes statically_complete_calculus Bot G Inf G (| =) Red IG Red FG and N . saturated N = ■ ⇒ ground_Inf_overapproximated N shows statically_complete_calculus Bot F Inf F (| = G ) Red I Red F

Adding Tiebreaker Orders

The completeness proofs for standard superposition and many other calculi are organized as a standard lifting. However, the lifted redundancy criterion cannot be used to justify the use of clause subsumption in provers. This points to a gap between theory and practice.

The saturation framework includes a generalization of standard lifting that bridges this gap. It relies on a wellfounded order, or more generally a family of orders, called tiebreaker. The tiebreaker can be instantiated with subsumption. In a given clause procedure, it can also be used to make a passive formula redundant w.r.t. the active version of the same formula.

The tiebreaker lifting is defined as an extension of standard lifting with a family Prec Fg of well-founded orders:

locale tiebreaker_lifting = empty_ord: standard_lifting Inf F Bot G Inf G (| =) Red IG Red FG Bot F G F G I + fixes Prec Fg :: ′ д ⇒ ′ f ⇒ ′ f ⇒ bool assumes minimal_element (Prec Fg д) UNIV
Redundancy of inferences Red I is as for the standard lifting, but redundancy of formulas can use the tiebreaker:

definition Red F :: ′ f set ⇒ ′ f set where Red F N = {C. ∀D ∈ G F C. D ∈ Red FG (G Fset N ) ∨ ∃E ∈ N . Prec Fg D E C ∧ D ∈ G F E}
Based on this definition, we proved that tiebreaker_lifting produces a nonground calculus.

The pen-and-paper development states that standard_ lifting produces a nonground calculus but points to the more general tiebreaker_lifting locale for a proof. To follow this structure, we interpreted standard_lifting as an instance of tiebreaker_lifting by taking Prec Fg := λд C C ′ . False, the empty tiebreaker family.

The tiebreaker order can be ignored when proving static completeness and recovered for dynamic completeness. Using the above construction, it was easy to prove formally:

theorem static_to_dynamic: statically_complete_calculus Bot F Inf F (| = G ) Red I empty_ord.Red F ← → dynamically_complete_calculus Bot F Inf F (| = G ) Red I Red F
The theorem holds because the definitions of saturation, fairness, and completeness depend on Red I but not on Red F , and because static and dynamic completeness are equivalent.

Intersection of Liftings

Ground calculi defined via the intersection of redundancy criteria can be lifted using the same general approach. The locale declaration is as follows:

locale lifting_intersection = inference_system Inf F + inference_system_family Q Inf Gq + consequence_relation_family Bot G Q entails q + fixes
Bot F :: ′ f set and G Fq :: ′ q ⇒ ′ f ⇒ ′ д set and G Iq :: ′ q ⇒ ′ f inference ⇒ ′ д inference set option and Prec Fg ::

′ д ⇒ ′ f ⇒ ′ f ⇒ bool assumes ∀q ∈ Q. tiebreaker_lifting Bot F Inf F Bot G (entails q q) (Inf Gq q) (Red Iq q) (Red Fq q) (G Fq q) (G Iq q) Prec Fg
For each index, we defined redundancy with and without tiebreaker order (Red IGq and either Red FGq or Red FGq∅ ) and entailment (entails Gq ) such that the intersection of the corresponding nonground calculi are also calculi:

sublocale intersection_calculus Bot F Inf F Q entails Gq Red IGq Red FGq sublocale empty_ord: intersection_calculus Bot F Inf F Q entails Gq Red IGq Red FGq∅
These commands introduce intersected notions of entailment (| = ∩G ) and redundancies (Red IG and either Red FG or empty_ord.Red FG ).

As in standard_lifting, the static completeness of the lifted intersection follows from that of the members of the ground family, and as in tiebreaker_lifting, the tiebreaker order can be ignored for static completeness:

theorem stat_eq_dyn_ref_comp_fam_inter:

statically_complete_calculus Bot F Inf F (| = ∩G ) Red I empty_ord.Red FG ← → dynamically_complete_calculus Bot F Inf F (| = ∩G ) Red I Red F
Although the proofs are theoretically easy and close to their informal counterparts, their formalization was complicated by the stack of locales and required tedious definition unfolding sequences and interpret commands to instantiate locales in the middle of proofs.

Adding Labels

The last kind of lifting attaches labels to formulas. These labels can be used to partition a set of formulas into its passive and active subsets. Finer partitions are also possible. The labels do not influence the formulas' semantics.

The locale extends tiebreaker_lifting with a set of labeled inferences Inf FL such that whenever an Inf F inference is possible, an Inf FL is also possible, and vice versa: lemma stat_ref_comp_to_labeled_sta_ref_comp:

locale labeled_tiebreaker_lifting = no_labels: tiebreaker_lifting Bot F Inf F Bot G (| =) Inf G Red IG Red FG G F G I Prec Fg + fixes Inf FL :: ( ′ f × ′ l) inference set assumes ι F ∈ Inf F = ■ ⇒ length Ls = length (prems_of ι F ) = ■ ⇒ ∃L 0 . Infer (zip (prems_of ι F ) Ls) (concl_of ι F , L 0 ) ∈ Inf FL and ι FL ∈ Inf FL = ■ ⇒ Infer (map fst (prems_of ι FL )) (fst (concl_of ι FL )) ∈ Inf F Bot FL :: ( ′ f × ′ l) set is defined as Bot F ×UNIV.
statically_complete_calculus Bot F Inf F (| = G ) no_labels.Red I no_labels.Red F = ■ ⇒ statically_complete_calculus Bot FL Inf FL (| = G L )
Red I Red F Labels can also be added to calculi that work with families of redundancy criteria. Since completeness results are independent of the tiebreaker order, we only considered the empty tiebreaker order: locale labeled_lifting_intersection = no_labels: lifting_intersection Inf F Bot G Q Inf Gq entails q Red Iq Red Fq Bot F G Fq G Iq (λд CL CL ′ . False) + fixes Inf FL ::

( ′ f × ′ l) inference set
We proved that static completeness with labels can be reduced to static completeness without labels.

Prover Architectures

Dynamic completeness is formulated in terms of an abstract single-formula-set prover ▷ (Section 2.4). In practice, saturation provers implement the given clause procedure described in the introduction. This simplifies bookkeeping: Instead of having to keep track of all possible n-ary inferences, actual provers only need to track active formulas.

The saturation framework includes two versions of the given clause procedure: an eager version called GC and a lazy version called LGC. LGC strictly generalizes GC, but because GC is sufficient for most applications and simpler to use, we formalized both separately (in Given_Clause_ Architectures.thy and Given_Clause_Architectures_ Revisited.thy).

Basic Setup

Much of the setup between GC and LGC can be shared, in a locale called given_clause_basis that extends labeled_ lifting_intersection. The locale assumes that the unlabeled version of the intersection calculus is complete: ≺ on unlabeled formulas that must be compatible with each other and with the grounding function:

assumes

C 1 • = D 1 = ■ ⇒ C 2 • = D 2 = ■ ⇒ C 1 • ≺ C 2 = ■ ⇒ D 1 • ≺ D 2 and q ∈ Q = ■ ⇒ C1 • = C2 = ■ ⇒ G Fq q C 1 = ■ ⇒ G Fq q C 2 and q ∈ Q = ■ ⇒ C2 • ≺ C1 = ■ ⇒ G Fq q C 1 = ■ ⇒ G Fq q C 2
In practice, • = would typically be α-equivalence, and • ≺ would be clause subsumption.

The locale also introduces an order ⊏ L on labels and a distinguished label active that must be minimal w.r.t. ⊏ L . Both • ≺ and ⊏ L are assumed to be well founded:

assumes minimal_element ( • ≺ ) UNIV and minimal_element (⊏ L ) UNIV
Inside the locale, we used • ≺ and ⊏ L to define a tiebreaker order ⊏ on labeled formulas and showed it to be well founded:

definition ⊏ ::

( ′ f × ′ l) ⇒ ( ′ f × ′ l) ⇒ bool where CL 1 ⊏ CL 2 ← → fst CL 1 • ≺ fst CL 2 ∨ (fst CL 1 • = fst CL 2 ∧ snd CL 1 ⊏ L CL 2 ) lemma wf_prec_FL: minimal_element (⊏) UNIV
This order can be used to strengthen the redundancy criterion of the labeled intersection calculus. For example, since (p(x), active) ⊏ (p(a), active) and (C, active) ⊏ (C, passive), for each pair the first labeled formula makes the second one redundant. Below, Red I and Red F refer to the strengthened criterion.

Finally, we present two lemmas that make explicit the relation between the labeled and unlabeled redundancy criteria:

lemma labeled_red_inf_eq_red_inf : ι ∈ Inf FL = ■ ⇒ ι ∈ Red I N ← → to_F ι ∈ no_labels.Red I (fst ' N ) lemma red_labeled_clauses: C ∈ no_labels.Red F (fst ' N ) ∨ (∃C ′ ∈ fst ' N . C ′ • ≺ C) ∨ (∃(C ′ , L ′ ) ∈ N . L ′ ⊏ L L ∧ C ′ • ≺ C) = ■ ⇒ (C, L) ∈ Red F N
Above, to_F denotes a function that erases all labels, and the infix operator ' denotes the image of a set under a function.

Although the first lemma is obvious when we compare the definitions of Red I and no_labels.Red I , the Isabelle proof is over 100 lines long. This is due mostly to the deep nesting of locales. The identity of notions is hidden under multiple layers of names, and Isabelle provides no proof automation that can unfold these definitions so as to reveal such connections. We conjecture that proof assistants based on computational type theories such as Agda, Coq, Lean, and Matita would cope more gracefully with these definitional equalities.

The given_clause_basis locale also ensures that inferences never produce active formulas. Only the procedure itself is allowed to make a formula active.

When we developed this locale and the two locales based on it, we did not immediately try to instantiate them. This led to an amusing incident when we attempted to verify RP. The given_clause_basis locale axioms turned out to be flawed. First, we had stated that •≻ must be well founded when we meant • ≺ . Strangely enough, we had successfully proved ⊏ well founded, even though it is based on • ≺ . How could that be? The answer is that we had relied on very powerful proof automation: Sledgehammer [START_REF] Paulson | Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers[END_REF]. That tool had discovered another flawed assumption and exploited it. This time, we had misspelled a constant's name. In Isabelle, this creates an implicitly universal variable. This convention, which certainly saves a lot of typing and is considered by some as an advantage of Isabelle over its rivals, had led to an inconsistent assumption.

The Eager Given Clause Procedure

The eager given clause procedure GC is described as a transition system that operates on labeled formula sets. This corresponds naturally to an inductive predicate GC :

inductive GC :: ( ′ f × ′ l) set ⇒ ( ′ f × ′ l) set ⇒ bool where process: N 1 = N ∪ M = ■ ⇒ N 2 = N ∪ M ′ = ■ ⇒ M ⊆ Red F (N ∪ M ′ ) = ■ ⇒ active_subset M ′ = ∅ = ■ ⇒ N 1 GC N 2 | infer: N 1 = N ∪ {(C, L)} = ■ ⇒ N 2 = N ∪ {(C, active)} ∪ M = ■ ⇒ L active = ■ ⇒ active_subset M = ∅ = ■ ⇒ no_labels.Inf_between (fst ' active_subset N ) {C} ⊆ no_labels.Red I (fst ' (N ∪ (C, active) ∪ M)) = ■ ⇒ N 1 GC N 2
The process rule can be used to add arbitrary passive formulas M ′ or to remove redundant formulas M. For example, the simplification of p(2 + 2) to p(4) would be modeled by taking M := {p(2 + 2)} and M ′ := {p(4)}. The infer rule selects a passive formula C-called the given formula or given clause-and makes it active. In addition, it draws all inferences between C and all the active formulas; more precisely, the rule requires the addition of enough passive formulas M to make these inferences redundant. The locale assumes that the inference system Inf F contains no nullary inferences.

The main benefit of using GC is that it makes it easier to draw inferences fairly. We only need to ensure that the prover eventually makes every passive formula active.

Via a refinement step, we showed that GC -transitions correspond to ▷-transitions. This was straightforward. Then we needed to connect GC's notion of fairness with the fair predicate on ▷-derivations (Section 2.4). Fairness for GC means that no formulas are passive at the limit, starting from a state in which no formulas are active: The informal proof is 13 lines long, but we needed 197 lines of Isabelle. The explanation for this poor De Bruijn factor is that the proof considers the maximal element of a set of integers, each representing a step in the derivation that is the first to satisfy a complex property for one of the premises of a given inference. The previous sentence already hints at the number of hidden reasoning steps necessary to obtain this particular element, although it is fairly easy to write the notion mathematically in a way that enables readers to build an adequate mental representation of the object. In Isabelle, however, every intermediate object in this construction must be shown to exist.

For each premise, the existence of the particular step of the derivation that verifies the property must be proved. This alone accounts for almost half of the proof. Then a set is built of those integers that must be proved nonempty and finite, before the maximal element can finally be obtained. The other half of the proof is dominated by the need to reason by elimination to identify that this particular step must be an infer step. This is obvious on paper by inspection of the transition rules but requires detailed reasoning in Isabelle.

We were not satisfied with this proof. A proof that is tedious to write is also tedious to read, and hides its insights from the reader. The situation reminded us of a 700-line Isabelle formalization by Fleury of an 8-line pen-and-paper proof by Weidenbach [START_REF] Christian Blanchette | A verified SAT solver framework with learn, forget, restart, and incrementality[END_REF]Section 4.3]. The solution in that case was to reason by invariance.

Can invariance help prove gc_fair in a more comprehensible way? It is well established that the given clause procedure satisfies the following key invariant: All inferences from active formulas are redundant w.r.t. the current set of formulas.

Initially, all formulas are passive, so the invariant holds vacuously. Whenever a given formula is made active, all inferences with active partners are made redundant, thereby maintaining the invariant. And if all formulas are active at the limit, then this means that all inferences from the entire limit N are redundant. Hence the derivation is fair and consequently N is saturated.

Paradoxically, although the invariant above is widely recognized as an important property of the given clause procedure, which is itself central in automated reasoning, we are not aware of any proofs in the literature that rely on it. Instead, the invariant is presented as a guide to intuition, if at all. For example, Bachmair and Ganzinger do not mention the invariant in their Handbook chapter.

In Isabelle, we defined the invariant as follows:

definition gc_invar ::

( ′ f × ′ l) set llist ⇒ enat ⇒ bool where gc_invar Ns i ← → Inf_from (active_subset (Liminf_upto Ns i)) ⊆ Sup_upto (lmap Red IG Ns) i
The predicate gc_invar Ns i determines whether the invariant holds at index i (which can be ∞). If k is within bounds, Liminf_upto Ns k is defined as the bounded limit inferior i k j=i Ns ! j, which is equal to the limit if k = ∞ and to Ns ! k otherwise. Similarly, Sup_upto Ns k is the bounded supremum k i Ns ! i. The invariant holds for all derivations with a reasonable initial state, and it extends to the limit:

lemma gc_invar_gc: chain ( GC ) Ns = ■ ⇒ active_subset (Ns ! 0) = ∅ = ■ ⇒ i < llength Ns = ■ ⇒ gc_invar Ns i lemma gc_invar_infinity: Ns [] = ■ ⇒ (∀i < llength Ns. gc_invar N s i) = ■ ⇒ gc_invar Ns ∞
Assuming that all formulas eventually become active, the invariant at the limit simplifies to Inf_from (Liminf Ns) ⊆ Sup (lmap Red IG Ns). This corresponds exactly to the definition of fairness, which is what we want.

The new formal proof is not much shorter in terms of number of lines (166 vs. 197), but it is much more compact horizontally and about half the size in bytes (7 kB vs. 13 kB). Written up as an informal proof, however, it is longer than the original; specifying the invariant and stating intermediate lemmas takes up vertical space. Even so, the new proof is more lucid, and we plan to include it in the journal version of Waldmann et al.

The Lazy Given Clause Procedure

The lazy given clause procedure LGC decouples inference scheduling and computation. Each inference ι is first added to a "to do" set T of scheduled inferences. At some later point, ι is computed, meaning that it is removed from T and its conclusion is added to the set N of labeled formulas. Alternatively, ι might be identified as redundant and deleted, a technique called orphan formula deletion. The formal definition of LGC follows:

inductive LGC ::

′ f inference set × ( ′ f × ′ l) set ⇒ ′ f inference set × ( ′ f × ′ l) set ⇒ bool where process: N 1 = N ∪ M = ■ ⇒ N 2 = N ∪ M ′ = ■ ⇒ M ⊆ Red F (N ∪ M ′ ) = ■ ⇒ active_subset M ′ = ∅ = ■ ⇒ (T , N 1 ) LGC (T , N 2 ) | schedule_infer: T 2 = T 1 ∪T ′ = ■ ⇒ N 1 = N ∪ {(C, L)} = ■ ⇒ N 2 = N ∪ {(C, active)} = ■ ⇒ L active = ■ ⇒ T ′ = no_labels.Inf_between (fst ' active_subset N ) {C} = ■ ⇒ (T 1 , N 1 ) LGC (T 2 , N 2 ) | compute_infer: T 1 = T 2 ∪ {ι} = ■ ⇒ N 2 = N 1 ∪ M = ■ ⇒ active_subset M = ∅ = ■ ⇒ ι ∈ no_labels.Red I (fst ' (N 1 ∪ M)) = ■ ⇒ (T 1 , N 1 ) LGC (T 2 , N 2 ) | delete_orphan_fmlas: T 1 = T 2 ∪ T ′ = ■ ⇒ T ′ ∩ no_labels.Inf_from (fst ' active_subset N ) = ∅ = ■ ⇒ (T 1 , N ) LGC (T 2 , N )
LGC has several benefits beyond orphan formula deletion. The "to do" set T can be used to support nullary inferences, or axioms. It can be used to represent infinite streams of inferences, which might for example result from higherorder unification (as in Zipperposition). Finally, inferences can often be stored more compactly than their conclusions, so LGC can be used to enable a low-level optimization (as in Waldmeister).

The key result is to show that LGC -derivations are fair under some reasonable assumptions: Compared with GC , an extra condition is added to ensure that all premise-free inferences are scheduled up front. The proof has the same structure as that of gc_fair, but the reasoning steps are more complex due to the extra rules and the presence of scheduled inferences. We needed 326 lines.

Can invariance help re-prove lgc_fair in the same way that it helped us with gc_fair? The lazy given clause procedure is little discussed in the literature, but it is easy to come up with a suitable generalization of the previous invariant: All inferences from active formulas are either scheduled in the "to do" set T or redundant w.r.t. the formula set N .

Initially, all formulas are passive, and all nullary inferences are in T , so the invariant holds. Whenever a given formula is made active, all inferences with active partners are scheduled, thereby maintaining the invariant. Removing an inference from T and computing it makes it redundant, preserving the invariant. Orphan formula deletion also preserves the invariant, because by definition an orphan cannot be derived from active formulas. And if T is empty and all formulas are active at the limit, then all inferences from the limit N are redundant, as required by fairness.

We defined the invariant as follows in Isabelle: definition lgc_invar ::

( ′ f inference set × ( ′ f × ′ l) set) llist ⇒ enat ⇒ bool where lgc_invar TNs i ← → Inf_from (active_subset (Liminf_upto (lmap snd TNs) i)) ⊆ from_F ' Liminf_upto (lmap fst TNs) i) ∪ Sup_upto (lmap (Red IG • snd) TNs) i
The formal proof by invariance resembles that for GC but with more cases to consider. Compared with the monolithic proof, we have a small improvement in number of lines (301 vs. 326) and a more substantial improvement in byte size (13 kB vs. 22 kB). For both GC and LGC, we believe the gain in lucidity is much higher than the numbers suggest.

Application to a Resolution Prover

A framework can hardly be called a framework until it is used. Waldmann et al. [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF]Example 29] applied their penand-paper framework to Bachmair and Ganzinger's resolution prover RP. To validate our formalized framework, a natural option was to apply it to RP as well, or rather RP's formalization by Schlichtkrull et al. We lifted ground static completeness explicitly and re-proved the dynamic completeness of RP. This example uses all the main components of the saturation framework and can serve as a blueprint for verifying other provers.

The Resolution Prover

Ordered resolution with selection, the calculus underlying RP, works on first-order clauses without equality (e.g., p(x) ∨ ¬ q(b, f(a))). It is parameterized by a well-order < on ground atoms, which is lifted to literals and clauses, and by a selection function S that maps each clause to one of its subclauses. The ground version of the calculus consists of a single n-ary inference rule:

C i ∨ A i ∨ • • • ∨ A i n i=1 ¬ A 1 ∨ • • • ∨ ¬ A n ∨ D C 1 ∨ • • • ∨ C n ∨ D
The duplicate atoms A i ∨ • • • ∨ A i in the n side premises are needed for completeness [START_REF] Bachmair | Resolution theorem proving[END_REF]Section 3]. Side conditions restrict the applicability of the rule, based on the well-order and the selection function. The order prunes the search space by identifying clauses that stray away from the goal (⊥). The selection function guides the search.

The nonground version of the inference rule is

C i ∨ A 1i ∨ • • • ∨ A ik i n i=1 ¬ A 1 ∨ • • • ∨ ¬ A n ∨ D (C 1 ∨ • • • ∨ C n ∨ D)σ
where σ is a most general simultaneous solution of all unification problems A i1

? = • • • ? = A ik i ? = A i , where 1 ≤ i ≤ n.
As in the ground case, further side conditions apply.

RP is defined as a transition system RP over states of the form S = (N, P, O), where N contains the "new" clauses, P contains the "processed" clauses, and O contains the "old" clauses. RP implements a variant of the given clause procedure, with N ∪ P as the passive set and O as the active set. RP is modeled naturally as an inductive predicate in Isabelle, with nine introduction rules: Informally, if we start in a state where all clauses are passive (i.e., O = ∅) and make sure that all clauses are active (i.e., N = P = ∅) at the limit, and the initial clause set is unsatisfiable, then ⊥ will belong to the limit. This, in turn, means that ⊥ is derived after finitely many transitions-ideally before the prover runs out of time and the user, of patience.

The The key to derive ⊥ is to resolve the initial clauses p(x, x) and ¬p(a, a). This requires moving both to O. Instead, the above derivation leaves ¬p(a, a) in P forever, focusing instead on generating useless clauses of the form p(x, f i (x)).

The Original Completeness Proof

The Isabelle completeness proof by Schlichtkrull et 4. As a corollary, since ground resolution is complete, if the initial clause set is unsatisfiable, then ⊥ occurs in the limit (grounded or not). It is difficult to relate to these proof steps. Even after the imprecisions in Bachmair and Ganzinger's proofs have been identified and clarified [21, Appendix A], the proof is hard to understand and remember. And yet, it is not very long. In the Handbook, it spans four pages. In Isabelle, it amounts to around 2500 lines, but this includes additional minor results. About half of the lines are dedicated to lifting ground inferences and coping with α-equivalence-issues that are only alluded to in the Handbook.

The New Completeness Proof

The new completeness proof (in FO_Ordered_Resolution_ Prover_Revisited.thy) has a more abstract flavor. It exploits the concepts presented in Sections 2 to 4. It also consists of four steps:

1. Ground resolution is statically complete. 2. Hence nonground resolution is statically complete.

3. Hence a given clause prover GC based on resolution is dynamically complete. 4. Thus, via refinement, RP is dynamically complete. The four steps are identified by letter codes: G (ground), F (first-order), FL (F with labels), and RP.

For step 1, if sufficed to show that ground resolution G_Inf is a clausal counterexample-reducing inference system (Sections 2.7 and 2.8). The core of the proof is a lemma already provided by Schlichtkrull et al.

For step 2, we defined nonground resolution as an inference system F_Inf. This could be done in one line in terms of the definition by Schlichtkrull et al. We also defined grounding functions: G F on clauses and G I on inferences.

The grounding of a clause C consists of all ground clauses of the form Cσ ; the grounding of an inference C n , . . . , C 1 ⊢ C 0 consists of all the inferences C n σ n , . . . , C 1 σ 1 ⊢ C 0 σ 0 ∈ G_Inf.

The main difficulty we encountered concerned the selection function. Recall that resolution is parameterized by a function S that restricts inferences. Inconveniently, S is generally not stable under substitution-it might behave differently on Cσ and C. Based on the limit set M, we can define an appropriate selection function S M for the ground level as a modification of S. However, this definition is circular: The limit M depends on the nonground calculus with its selection function S, which in turn is lifted from a ground calculus with its selection function S M , which depends on M.

Remarkably, this circularity had initially escaped the attention of Waldmann et al. as they worked in L A T E X. It is all too easy to dismiss selection as an orthogonal concern. We noticed the issue only as we formalized RP. Fortunately, it was not too late to adapt the pen-and-paper framework before it was published [START_REF] Waldmann | A comprehensive framework for saturation theorem proving[END_REF].

The notion of intersection of redundancy criteria (Section 2.5) was designed to break the circularity. Instead of being lifted from S M , where M is the limit, the nonground calculus is lifted simultaneously from all selection functions of the form S M , where M is an arbitrary clause set. This was achieved formally by instantiating the lifting_intersection locale (Section 2.5) and showing that the grounding functions G F and G I satisfy basic properties.

We could then instantiate statically_complete_calculus (Section 2.4) to lift the ground calculus to the nonground level. The key lemma states that any inference ι G from the grounded clauses is approximated at the nonground level by an inference ι F :

lemma G_Inf_overapprox_F_Inf : ι G ∈ G. Inf_from M ( (G F ' M)) = ■ ⇒ ∃ι F ∈ F. Inf_from M. ι G ∈ G I M ι F
For the core of the proof, we could again reuse a result from Schlichtkrull et al. This illustrates again how the saturation framework takes care of the bureaucracy and allows the user to focus on the calculus-specific reasoning.

Step 3 is about deriving dynamic completeness of a given clause procedure. We needed to define a suitable equivalence relation • = and tiebreaker order • ≺ in formulas. We also defined the labels New, Processed, and Old (= active) and defined the order ⊏ L such that New ⊐ L Processed ⊐ L Old. With these definitions in place, we instantiated given_clause and retrieved two main results: (1) the induced GC refines ▷ and (2) the induced GC is dynamically complete.

Step 4 was essentially a refinement proof: RP's states, which are triples of clause sets, must be converted to GC's labeled clause sets: definition lclss_of :: The first eight transition rules of RP can be simulated by the process rule of GC, and the last rule of RP can be simulated by infer. To illustrate this, we will sketch the proof for the first RP rule, which deletes tautologies. Consider the transition (N ∪ {C}, P, O) RP (N, P, O), where {Neg A, Pos A} ⊆ C. We need to prove that there exist labeled clause sets N ′ , M, M ′ such that N ′ ∪M GC N ′ ∪M ′ by the process rule. This amounts to showing that (1) M is redundant w.r.t. N ′ ∪ M ′ and (2) no clause from M ′ is labeled active. We take N ′ := lclss_of (N, P, O), M := {(C, New)}, and M ′ := ∅. Condition (1) is obvious since C is a tautology, and ( 2) is vacuously true.

After completing step 4, we had all the results we needed to re-prove the main theorem, RP_complete_if_fair-with one exception. To lighten the presentation, we used our notations for basic concepts such as inferences, redundancy, and fairness. However, Schlichtkrull et al. used slightly different formulations, based on Bachmair and Ganzinger. Their notions-prefixed by "old" in our theory files to clearly identify them-are restricted to clauses, which is not an issue for RP, but the side premises of an inference are stored in a multiset and thus unordered. This affects all definitions based on inferences, from redundancy to saturation. We first proved completeness and related results using our concepts; then we restated the results and re-proved them using theirs, as a sanity check. And although we were mostly interested in completeness, we also proved the soundness of RP derivations, exploiting the lemma unsat_limit_iff (Section 2.6).

Discussion

The approach taken for the new proof can be applied with little change to other saturation calculi based on resolution or superposition. For calculi like constraint superposition that cannot be obtained as the lifting of a ground calculus, steps 1 and 2 must be replaced by a monolithic proof that the nonground calculus is complete.

Is the new proof an improvement over the one by Schlichtkrull et al.? It certainly is in terms of lines of source text. Let us ignore soundness and the conversions between basic concepts, and all the definitions and lemmas that are shared between the two proofs, including the definition of RP itself. Then we arrive at around 700 lines for the new proof compared with 1200 lines for the original proof. Among the 700 lines, nearly half are concerned with the refinement from GC to RP. But regardless of the line counts, we are convinced that the new proof's modularity makes it more intelligible and easier to teach, and easier to mimic to formally verify other saturation provers.

Looking at the line counts, one might be led to believe that the new proof was easy to develop. Unfortunately, this was not the case, because we worked with a less mature version of the framework. The circularity issue noted above led to a one-year hiatus, and when we resumed, we still had to find our way across a web of locales. The main difficulty we faced was that several copies of the same locale instances emerged, identical up to unfolding of definitions but distinct as far as the locale machinery is concerned. Instantiating the given_clause locale, which pulls in a wide range of concepts, initially produced around 40 subgoals instead of the 14 we now get. There were so many layers of definitions that Sledgehammer was helpless.

One reason locales became so complicated is that we rigorously followed the informal proofs by reduction. For example, lifting with a tiebreaker order is reduced to lifting with ∅ as the tiebreaker, which in turn amounts to a standard lifting. A more direct proof would consider only the most general concept and avoid the replication of concepts. Fortunately, we found a way to simplify the locales while keeping compatibility with the informal argument. Often, it sufficed to replace an opaque definition by a transparent abbreviation, or to choose a canonical locale instance and refrain from using the other definitionally equal instances.

Locales are truly a double-edged sword. On the one hand, they conveniently keep track of parameters and dependencies; without them, we would need to clutter definitions with extra arguments and lemmas with extra assumptions. On the other hand, locales often surprised us and provide too few introspection methods. Two examples: First, when instantiating a locale, we know of no easy way to figure where the n subgoals come from in the locale hierarchy. Second, after instantiating a locale, the command print_theorems, which is designed to display the lemmas introduced by the previous command, prints nothing. So after closing the 14 subgoals of given_clause, we still have to search for what we have proved. Locales are immensely useful, but they could be made easier to use and debug.

Concluding Remarks

We formalized in Isabelle/HOL a framework designed to support the verification of automatic provers based on saturation calculi. This work joins a long list of verifications of logical calculi and theorem provers; we refer to Blanchette [10, Section 5] for a recent overview of related work. But unlike virtually all the previous work, instead of focusing on a single calculus or prover, we mechanized a framework applicable to a wide range of provers.

Because the informal proof and its formalization took place partly in parallel, they could benefit from each other. The precise and reliable informal proof was mostly a joy to translate into Isar. The formalization did unveil an unpleasant circularity in the application of the framework to RP, which was resolved by introducing a new concept. But we also encountered the opposite situation, where it was the translation to Isabelle that contained flawed conditions. We uncovered this also thanks to the RP case study.

The pen-and-paper version of the framework, due to Waldmann et al., is already being used in seven separate informal proofs in ongoing work by colleagues and ourselves. If we want our formalized framework to be useful in the same way, we first need to prove ground static completeness for various interesting saturation calculi. So far, only ordered resolution and, thanks to Peltier [START_REF] Peltier | A variant of the superposition calculus[END_REF], a variant of standard superposition have been formalized in Isabelle.

Beyond our framework, the IsaFoR (Isabelle Formalization of Rewriting) library [START_REF] Thiemann | Certification of termination proofs using CeTA[END_REF] and the RP formalization [START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's ordered resolution prover[END_REF] offer many definitions and lemmas related to first-order terms and clauses. Starting from RP, Schlichtkrull et al. [START_REF] Schlichtkrull | A verified prover based on ordered resolution[END_REF] performed three further refinement steps to derive an executable functional prover, RPx, in Standard ML. With no effort, RPx could be rebased to use our RP proof. In principle, it should be possible to refine RPx further to use optimized data structures and algorithms, following the lines of Fleury's verification of an imperative SAT solver using Isabelle [START_REF] Fleury | Optimizing a verified SAT solver[END_REF].

Waldmann et al. present a wealth of examples, especially in their technical report. For future work, some of these could be formalized. Particularly useful would be their three prover loops (Otter, DISCOUNT, and Zipperposition) based on the given clause procedures GC and LGC. Choosing one of these loops instead of GC or LGC as the basis of a prover could reduce the refinement burden. Using Peltier's formalization of superposition, it should now be possible to verify a superposition prover in the style of RPx in a few thousand lines of Isabelle. Integrating imperative data structures and algorithms, however, would involve much more work, perhaps of the order of a PhD project.

The saturation framework is very flexible, but it does not capture the important technique of clause splitting as implemented in SPASS and Vampire [START_REF] Fietzke | Labelled splitting[END_REF][START_REF] Voronkov | AVATAR: The architecture for first-order theorem provers[END_REF]. The notion of redundancy criterion is also too weak to justify pure literal and blocked clause elimination [START_REF] Järvisalo | Blocked clause elimination[END_REF]. To lift these restrictions, more theoretical research is necessary. If the present work is an indication of anything, this research should be carried out at least in part using a proof assistant.

  where G Fset :: ′ f set ⇒ ′ д set is the lifting of G F to sets. This relation is called Herbrand entailment. For first-order logic, it coincides with the familiar Tarski entailment when N 2 = {⊥}, allowing us to use | = G in a refutational setting. For example, {p(x), ¬ p(a)} | = G {⊥}.

  The grounding functions (G IL and G FL ) and the entailment relation (| = G L ) simply ignore labels. The main result lets us derive the static completeness of the labeled calculus from the static completeness of the base calculus:

  assumes statically_complete_calculus Bot F Inf F (| = ∩G ) no_labels.Red I no_labels.Red F It introduces an equivalence relation • = and an order •

  lemma gc_fair: assumes chain ( GC ) Ns and active_subset (Ns ! 0) = ∅ and passive_subset (Liminf Ns) = ∅ shows fair Ns

  lemma lgc_fair: assumes chain ( LGC ) TNs and active_subset (snd (TNs ! 0)) = ∅ and passive_subset (Liminf (lmap snd TNs)) = ∅ and ∀ι ∈ Inf F . prems_of ι = [] -■ → ι ∈ fst (TNs ! 0) and Liminf (lmap fst TNs) = ∅ shows fair (lmap snd TNs)

  inductive RP :: ′ a state ⇒ ′ a state ⇒ bool where {Neg A, Pos A} ⊆ C = ■ ⇒ (N ∪ {C}, P, O) RP (N, P, O)| D ∈ P ∪ O = ■ ⇒ subsumes D C = ■ ⇒ (N ∪ {C}, P, O) RP (N, P, O) | D ∈ N = ■ ⇒ strict_subsumes D C = ■ ⇒ (N, P ∪ {C}, O) RP (N, P, O) | D ∈ N = ■ ⇒ strict_subsumes D C = ■ ⇒ (N, P, O ∪ {C}) RP (N, P, O) | D ∈ P ∪ O = ■ ⇒ reduces D C L = ■ ⇒ (N ∪ {C ⊎ {L}}, P, O) RP (N ∪ {C}, P, O) | D ∈ N = ■ ⇒ reduces D C L = ■ ⇒ (N, P ∪ {C ⊎ {L}}, O) RP (N, P ∪ {C}, O) | D ∈ N = ■ ⇒ reduces D C L = ■ ⇒ (N, P, O ∪ {C ⊎ {L}}) RP (N, P ∪ {C}, O) | (N ∪ {C}, P, O) RP (N, P ∪ {C}, O) | (∅, P ∪ {C}, O) RP (concl_of ' Inf_between O {C}, P, O ∪ {C})The first seven rules perform optional clause processing steps: tautology elimination, clause subsumption, and clause reduction (i.e., removal of needless literals). The next-to-last rule moves a clause C from N to P, and the last rule moves C further from P to O and computes all possible inferences between C and partners from O. A sequence of states Ss is called fair, written fair Ss, if N_of (Liminf Ss) = P_of (Liminf Ss) = ∅. The completeness theorem for RP can be stated as follows: theorem RP_complete_if_fair: assumes chain ( RP ) Ss and O_of (Ss ! 0) = ∅ and fair Ss and ∀I . ¬ I | = G S (Ss ! 0) shows ⊥ ∈ O_of (Liminf Ss)

  following RP derivation [21, Section 3], starting from an unsatisfiable clause set, illustrates what can go wrong without fairness: ({¬p(a, a), p(x, x), ¬p(f(x), y) ∨ p(x, y)}, ∅, ∅) + RP (∅, {¬p(a, a), p(x, x), ¬p(f(x), y) ∨ p(x, y)}, ∅) RP (∅, {¬p(a, a), p(x, x)}, {¬p(f(x), y) ∨ p(x, y)}) RP ({p(x, f(x))}, {¬p(a, a)}, {¬p(f(x), y) ∨ p(x, y), p(x, x)}) RP (∅, {¬p(a, a), p(x, f(x))}, {¬p(f(x), y) ∨ p(x, y), p(x, x)}) RP ({p(x, f(f(x)))}, {¬p(a, a)}, {¬p(f(x), y) ∨ p(x, y), p(x, x), p(x, f(x))}) RP • • •

  ′ a state ⇒ ( ′ a clause × label) set where lclss_of S = (λC. (C, New)) ' N_of S ∪ (λC. (C, Processed)) ' P_of S ∪ (λC. (C, Old)) ' O_of S

  saturation calculi work with clauses. In Isabelle, we reuse the representation of clauses as finite multisets of literals introduced by Schlichtkrull et al. [21, Section 2.3]. The empty clause ⊥ is represented by ∅, but we will continue to write ⊥. We take Bot = {⊥}. Literals over atoms of type

′ a take the form Pos A or Neg A, where A :: ′ a. In the literature, sets are sometimes used instead of multisets to represent clauses, but multisets are more suitable for resolution-and superposition-like calculi because the size of a multiset is invariant under substitution.

  al. (in FO_ Ordered_Resolution.thy and FO_Ordered_Resolution_ Prover.thy), based on Bachmair and Ganzinger, consists of the following sequence of steps:1. An RP -transition from S to S ′ corresponds to a ▷transition from G S S to G S S ′ , where G S returns, for a given state, the set consisting of the G F -groundings of all the clauses in the state. 2. Let Ss be a fair RP derivation. Then any nonredundant clause C in Ss's ground projection eventually reaches O and stays there.3. Moreover, if O is initially empty, then the limit of the G S -grounding of Ss is saturated.

To use our theories with Isabelle2020, check out revision a61b4f25e279 of the development repository of the AFP, hosted at https://foss.heptapod.net/ isa-afp/afp-devel.

Acknowledgments

We thank Alexander Bentkamp, Martin Desharnais, Robert Lewis, Simon Robillard, Anders Schlichtkrull, Mark Summerfield, Dmitriy Traytel, Uwe Waldmann, and the anonymous reviewers for their comments and suggestions.

Blanchette's research has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). He has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).