Anders Schlichtkrull

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

Dmitriy Traytel
email: traytel@inf.ethz.ch

A Verified Prover Based on Ordered Resolution

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

The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional first-order ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.

Introduction

Automatic theorem provers based on superposition, such as E [START_REF] Schulz | System Description: E 1.8[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], are often employed as backends in proof assistants and program verification tools [START_REF] Bobot | Why3: Shepherd Your Herd of Provers[END_REF][START_REF] Kovács | Finding Loop Invariants for Programs over Arrays using a Theorem Prover[END_REF][START_REF] Paulson | Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers[END_REF]. Superposition is a highly successful calculus for first-order logic with equality, which generalizes both ordered resolution [START_REF] Bachmair | Resolution Theorem Proving[END_REF] and ordered completion [START_REF] Bachmair | Completion without Failure[END_REF].

Resolution operates on sets of clauses. A clause is an nary disjunction of literals L 1 ∨ • • • ∨ L n whose variables are interpreted universally. Each literal is either an atom A or its negation ¬A. An atom is a symbol applied to a tuple of terms-e.g., prime(n). The empty clause is denoted by ⊥.

Resolution works by refutation: Conceptually, the calculus proves a conjecture ∀ x . C from a set of axioms D by deriving ⊥ from D ∪ {∃ x . ¬C}, indicating its unsatisfiability. As an optimization, it uses a redundancy criterion to discard tautologies, subsumed clauses, and other unnecessary clauses; for example, p(x) ∨ q(x) and p(5) are both subsumed by p(x). Compared with plain resolution, ordered resolution relies on an order on the atoms to further prune the search space.

Modern superposition provers are highly optimized programs that rely on sophisticated calculi, with a rich metatheory. In this paper, we propose to verify, using Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF], a purely functional prover based on ordered resolution. Although our primary interest is in metatheory per se, there are of course applications for verified provers [START_REF] Thiemann | Extending a Verified Simplex Algorithm[END_REF].

The verification relies on stepwise refinement [START_REF] Wirth | Program Development by Stepwise Refinement[END_REF]. Four layers are connected by three refinement steps.

Our starting point, layer 1 (Section 3), is an abstract Prologstyle nondeterministic resolution prover in a highly general form, as presented by Bachmair and Ganzinger [START_REF] Bachmair | Resolution Theorem Proving[END_REF] and as formalized in our earlier work [START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's Ordered Resolution Prover[END_REF][START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover[END_REF]. It operates on possibly infinite sets of clauses. Its soundness and refutational completeness are inherited by the other layers.

Layer 2 (Section 4) operates on finite multisets of clauses and introduces a priority queue to ensure that inferences are performed in a fair manner, guaranteeing completeness: Given a valid conjecture, the prover will eventually derive ⊥.

Layer 3 (Section 5) is a deterministic program that works on finite lists, committing to a strategy for assigning priorities to clauses. However, it is not fully executable: It abstracts over operations on atoms and employs logical specifications instead of executable functions for auxiliary notions.

Finally, layer 4 (Section 6) is a fully executable program. It provides a concrete datatype for atoms and executable definitions for all auxiliary notions, including unifiers, clause subsumption, and the order on atoms.

From layer 4, we can extract Standard ML code by invoking Isabelle's code generator [START_REF] Haftmann | Code Generation via Higher-Order Rewrite Systems[END_REF]. The resulting prover constitutes a proof of concept: It uses an efficient calculus (layer 1) and a reasonable strategy to ensure fairness (layers 2 and 3), but depends on inefficient list-based data structures. Further refinement steps will be required to obtain a prover that is competitive with the state of the art.

The refinement steps connect vastly different levels of abstraction. The most abstract level is occupied by an infinitary logical calculus and the semantics of first-order logic. Soundness and completeness relate these two notions. At the functional programming level, soundness amounts to a safety property: Whenever the program terminates normally, its outcome is correct, whether it is a proof or a finite saturation witnessing unprovability. Correspondingly, refutational completeness is a liveness property: If the conjecture is valid, the program will always terminate normally. We find that, far from being academic exercises, Bachmair and Ganzinger's framework [START_REF] Bachmair | Resolution Theorem Proving[END_REF] and its formalization [START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's Ordered Resolution Prover[END_REF][START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover[END_REF] adequately capture the metatheory of actual provers.

To our knowledge, our program is the first verified prover for first-order logic implementing an optimized calculus. It is also the first example of the application of refinement in a first-order context. This methodology has been used to verify SAT solvers [START_REF] Christian Blanchette | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality[END_REF][START_REF] Marić | Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle/HOL[END_REF], which decide the satisfiability of propositional formulas, but first-order logic is semidecidable-sound and complete provers are guaranteed to terminate only for unsatisfiable (i.e., provable) clause sets. This complicates the transfer of completeness results across refinement layers.

The present work is part of the IsaFoL (Isabelle Formalization of Logic) project, 1 which 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[END_REF]. The Isabelle files are available in the Archive of Formal Proofs [START_REF] Schlichtkrull | A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover[END_REF][START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's Ordered Resolution Prover[END_REF] and in the IsaFoL repository. 2 The parts specific to the functional prover refinement amount to about 4000 lines of source text. A convenient way to study the files is to open them in Isabelle/jEdit [START_REF] Wenzel | Isabelle/jEdit-a Prover IDE within the PIDE Framework[END_REF], as explained in the repository's readme file. The files were created using Isabelle version 2018, but the repositories will be updated to follow Isabelle's evolution.

Atoms and Substitutions

The first three refinement layers are based on an abstract library of first-order atoms and substitutions. In the fourth and final layer, the abstract framework is instantiated with concrete datatypes and functions.

We start from IsaFoL's library of clausal logic [START_REF] Christian Blanchette | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality[END_REF], which is parameterized by a type ′ a of logical atoms. Literals L are defined as an inductive datatype: ′ a literal = Pos ′ a | Neg ′ a. The type of clauses C, D, E is introduced as the alias ′ a clause = ′ a literal multiset, where multiset is the type constructor of finite multisets. Thus, the clause ¬ A∨B, where A and B are arbitrary atoms, is represented by the multiset {Neg A, Pos B}, and the empty clause ⊥ is represented by the empty multiset ∅. The complement operation is defined as -Neg A = Pos A and -Pos A = Neg A for any atom A.

In automated reasoning, it is customary to view clauses as multisets of literals rather than as sets. One reason is that multisets behave more naturally under substitution. For example, applying {y → x } to the two-literal clause p(x)∨p(y) results in p(x) ∨ p(x), which preserves the clause's structure.

The truth value of ground (i.e., variable-free) atoms is given by a Herbrand interpretation: a set I , of type ′ a set, of all true ground atoms. The "models" predicate | = is defined as

I | = A ⇐ ⇒ A ∈ I .
This definition is lifted to literals, clauses, and sets of clauses in the usual way. A set of clauses D is satisfiable if there exists an interpretation I such that I | = D.

Resolution depends on a notion of substitution and of most general unifier (MGU). These auxiliary concepts are provided by a third-party library, IsaFoR (Isabelle Formalization of Rewriting) [START_REF] Thiemann | Certification of Termination Proofs using CeTA[END_REF]. To reduce our dependency on external libraries, we hide them behind abstract locales parameterized by a type of atoms ′ a and a type of substitutions ′ s.

We start by defining a locale substitution_ops that declares application (•), identity (id), and composition (•):

locale substitution_ops = fixes id :: ′ s and • :: ′ s ⇒ ′ s ⇒ ′ s and • :: ′ a ⇒ ′ s ⇒ ′ a Within the locale's scope, we introduce a number of derived concepts. Ground atoms are defined as those atoms that are left unchanged by substitutions: is_ground A ⇐ ⇒ ∀σ. A = A • σ . A ground substitution is a substitution whose application always results in ground atoms. Nonstrict and strict generalization are defined as

generalizes A B ⇐ ⇒ ∃σ. A • σ = B strictly_generalizes A B ⇐ ⇒ generalizes A B ∧ ¬ generalizes B A
The operators on atoms are lifted to literals, clauses, and sets of clauses. The grounding of a clause is defined as

grounding_of C = {C • σ | is_ground σ }
The operator is lifted to sets of clauses in the obvious way. Clause subsumption is defined as

subsumes C D ⇐ ⇒ ∃σ. C • σ ⊆ D
with strictly_subsumes as its strict counterpart. The next locale, substitution, characterizes the operations defined by substitution_ops. A separate locale is necessary because we cannot interleave assumptions and definitions in a single locale. In addition, substitution fixes a function for renaming clauses apart (so that they do not share any variables) and a function that, given a list of atoms, constructs an atom with these as subterms:

locale substitution = substitution_ops + fixes renamings_apart :: ′ a clause list ⇒ ′ s list and atm_of_atms ::

′ a list ⇒ ′ a assumes A • id = A A • (σ • τ ) = (A • σ ) • τ (∀A. A • σ = A • τ ) = ■ ⇒ σ = τ is_ground (C • σ ) = ■ ⇒ ∃τ . is_ground τ ∧ C • τ = C • σ wf strictly_generalizes |renamings_apart Cs| = |Cs| ρ ∈ renamings_apart Cs = ■ ⇒ is_renaming ρ var_disjoint (Cs • renamings_apart Cs) atm_of_atms As • σ = atm_of_atms Bs ⇐ ⇒ map (λA. A • σ ) As = Bs
The above definition is presented to give a flavor of our development. We refer to the Isabelle files for the exact definitions. Inside the locale, we prove further properties of the substitution_ops operations. Notably, we prove wellfoundedness of the strictly_subsumes predicate based on the well-foundedness of strictly_generalizes, which is stated as an assumption. The atm_of_atms operation is used to encode a clause as a single atom in this well-foundedness proof.

Finally, a third locale, mgu, extends substitution by fixing a function mgu :: ′ a set set ⇒ ′ s option that computes an MGU σ given a set of unification constraints.

Bachmair and Ganzinger's Prover

Our earlier formalization [START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's Ordered Resolution Prover[END_REF][START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover[END_REF] of a nondeterministic ordered resolution prover presented by Bachmair and Ganzinger [START_REF] Bachmair | Resolution Theorem Proving[END_REF] forms layer 1 of our refinement. In this paper, we restrict our focus to binary resolution, which can be implemented efficiently and forms the basis of modern provers.

The ordered resolution calculus is parameterized by a total order > ("larger than") on ground atoms. For first-order logic, the order > is extended to an order ≻ on nonground atoms so that B ≻ A if and only if for all ground substitutions σ , we have B • σ > A • σ . The calculus consists of the single rule

C ∨ A 1 ∨ • • • ∨ A k ¬A ∨ D (C ∨ D) • σ where σ is the (canonical) MGU that solves the unification problem A 1 ? = • • • ? = A k ? = A.
In addition, each A i • σ must be strictly ≻-maximal with respect to the atoms in C • σ (meaning that A i is not ⪯ any atom in C • σ ), and A • σ is ≻-maximal with respect to the atoms in D • σ . To achieve completeness, the rule must be adapted slightly to rename apart the variables occurring in different premises.

A set of clauses D is saturated if any conclusion from premises in D is already in D. The ordered resolution calculus is refutationally complete, meaning that any unsatisfiable saturated set of clauses necessarily contains ⊥.

Resolution provers start with a finite set of initial clausesthe input problem-and successively add conclusions from premises in the set. If the inference rule is applied in a fair fashion, the set reaches saturation at the limit; if the set is unsatisfiable, this means ⊥ is eventually derived.

Crucially, not only do efficient provers add clauses to their working set, they also remove clauses that are deemed redundant. This requires a refined notion of saturation. We call a set of clauses D saturated up to redundancy, written saturated_upto D, if any inference from nonredundant clauses in D yields a redundant conclusion.

Bachmair and Ganzinger's nondeterministic first-order prover, called RP, captures the "dynamic" aspects of saturation. RP is defined as an inductive predicate on states, which are triples S = (N , P, O) of new clauses N, processed clauses P, and old clauses O. Initially, N is the input problem, and P ∪ O is empty. Clauses can be removed if they are tautological or subsumed or after subsumption resolution has been applied. When all clauses in N have been processed (either removed entirely or moved to P), a clause C from P can be chosen for inference computation: C is then moved from P to O, and all its conclusions with premises from the other old clauses form the new N. Formally:

inductive :: ′ a state ⇒ ′ a state ⇒ bool where Neg A ∈ C ∧ Pos A ∈ C = ■ ⇒ (N ∪ {C}, P, O) 1 (N , P, O) | D ∈ P ∪ O ∧ subsumes D C = ■ ⇒ (N ∪ {C}, P, O) 2 (N , P, O) | D ∈ N ∧ strictly_subsumes D C = ■ ⇒ (N , P ∪ {C}, O) 3 (N , P, O) | D ∈ N ∧ strictly_subsumes D C = ■ ⇒ (N , P, O ∪ {C}) 4 (N , P, O) | D ∈ P ∪ O ∧ reduces D C L = ■ ⇒ (N ∪ {C ⊎ {L}}, P, O) 5 (N ∪ {C}, P, O) | D ∈ N ∧ reduces D C L = ■ ⇒ (N , P ∪ {C ⊎ {L}}, O) 6 (N , P ∪ {C}, O) | D ∈ N ∧ reduces D C L = ■ ⇒ (N , P, O ∪ {C ⊎ {L}}) 7 (N , P ∪ {C}, O) | (N ∪ {C}, P, O) 8 (N , P ∪ {C}, O) | (∅, P ∪ {C}, O) 9 (concl_of ' infers_between O C, P, O ∪ {C})
Subscripts on identify the rules. The notation f ' X stands for the image of X under f , infers_between O C calculates all the ordered resolution inferences whose premises are a subset of O ∪ {C} that contains C, and reduces D C L is defined as

∃D ′ L ′ σ. D = D ′ ⊎{L ′ } ∧ -L = L ′ •σ ∧ D ′ •σ ⊆ C.
The following derivation shows that RP can diverge even on unsatisfiable clause sets:

({¬p(a, a), p(x, x), ¬p(f(x), y) ∨ p(x, y)}, ∅, ∅) + 8 (∅, {¬p(a, a), p(x, x), ¬p(f(x), y) ∨ p(x, y)}, ∅) 9 (∅, {¬p(a, a), p(x, x)}, {¬p(f(x), y) ∨ p(x, y)}) 9 ({p(x, f(x))}, {¬p(a, a)}, {¬p(f(x), y) ∨ p(x, y), p(x, x)}) 8 (∅, {¬p(a, a), p(x, f(x))}, {¬p(f(x), y) ∨ p(x, y), p(x, x)}) 9 ({p(x, f(f(x)))}, {¬p(a, a)}, {¬p(f(x), y) ∨ p(x, y), p(x, x), p(x, f(x))}) 8 • • •
We can leave ¬p(a, a) in P forever and always generate more clauses of the form p(x, f i (x)), for increasing values of i. This emphasizes the importance of a fair strategy for selecting clauses to move from P to O using rule 9. Formally, a derivation is a possibly infinite sequence of states S 0 S 1 S 2 • • • . In Isabelle, this is expressed by the codatatype of lazy lists:

codatatype ′ a llist = LNil | LCons ′ a ( ′ a llist)
Lazy list operation names are prefixed by an L or l to distinguish them from the corresponding operations on finite lists. For example, lhd xs yields xs's head (if xs LNil), and lnth xs i yields the (i + 1)st element of xs (if i < |xs|).

We capture the mathematical notation S 0 S 1 • • • formally as chain ( ) Ss, where Ss is a lazy list of states and chain is a coinductive predicate:

coinductive chain :: ( ′ a ⇒ ′ a ⇒ bool) ⇒ ′ a llist ⇒ bool where chain R (LCons x LNil) | chain R xs ∧ R x (lhd xs) = ■ ⇒ chain R (LCons x xs)
Coinduction is used to allow infinite chains. The base case is needed to allow finite chains. Chains cannot be empty. Another important notion is that of the limit of a sequence Xs of sets. It is defined as the set of elements that are members of all positions of Xs except for an at most finite prefix:

definition Liminf :: ′ a set llist ⇒ ′ a set where Liminf Xs = i < |Xs | j:i ≤j < |Xs | lnth Xs j
Liminf and other operators working on clause sets are lifted pointwise to states. For example, the limit of a sequence of states is defined as Liminf Ss = (Liminf Ns, Liminf Ps, Liminf Os), where Ns, Ps, and Os are the projections of the N , P, and O components of Ss.

The soundness theorem states that if RP derives ⊥ (i.e., ∅) from a set of clauses, that set must be unsatisfiable:

theorem RP_sound: ∅ ∈ clss_of (Liminf Ss) = ■ ⇒ ¬ satisfiable (grounding_of (lhd Ss))
In the above, clss_of (N , P, O) = N ∪ P ∪ O.

A stronger, finer-grained notion of soundness relates models before and after a transition:

theorem RP_model: S S ′ = ■ ⇒ (I | = grounding_of S ′ ⇐ ⇒ I | = grounding_of S)
The canonical way of expressing the unsatisfiability of a set or multiset of first-order clauses with respect to Herbrand interpretations is as the unsatisfiability of its grounding.

Completeness of the prover can only be guaranteed when its rules are executed in a fair order, such that clauses do not get stuck forever in N or P. Accordingly, fairness is defined as Liminf Ns = Liminf Ps = ∅. The completeness theorem states that the limit of a fair derivation Ss is saturated:

theorem RP_saturated_if _fair: fair Ss = ■ ⇒ saturated_upto (Liminf (grounding_of Ss))
In particular, if the initial problem is unsatisfiable, ⊥ must appear in the O component of the limit of any fair derivation:

corollary RP_complete_if _fair: fair Ss ∧ ¬ satisfiable (grounding_of (lhd Ss)) = ■ ⇒ ∅ ∈ O_of (Liminf Ss)

Ensuring Fairness

The second refinement layer is the prover RP w , which ensures fairness by assigning a weight to every clause and by organizing the set of processed clauses-the P state component-as a priority queue, where lighter clauses are chosen first. By assigning somewhat heavier weights to newer clauses, we can guarantee that all derivations are fair.

Another necessary ingredient for fairness is that derivations must be complete. For example, the incomplete derivation consisting of the single state ({C}, ∅, ∅) is not fair. This requirement is expressed formally as full_chain ( w ) Ss.

For the rest of this section, we fix a full chain Ss such that P_of (lhd Ss) = O_of (lhd Ss) = ∅.

Because each RP w rule corresponds to an RP rule, it is straightforward to lift the soundness and completeness results from RP to RP w . The main difficulty is to show that the priority queue ensures fairness of full derivations, which is needed to obtain an unconditional completeness theorem for RP w , without the assumption fair Ss.

Definition. The weight of a clause C, which defines its priority in the queue, may depend both on the clause itself and on when it was generated. To reflect this, the RP w prover represents clauses by a pair (C, i), where i is the timestamp. The larger the timestamp, the newer the clause. A state is now a quadruple S = (N , P, O, t), where the first three components are finite multisets and t is the timestamp to assign to the next generation of clauses. Formally, we have the following type abbreviations:

type_synonym ′ a wclause = ′ a clause × nat type_synonym ′ a wstate = ′ a wclause multiset × ′ a wclause multiset × ′ a wclause multiset × nat
We extend the FO_resolution_prover locale, in which RP is defined, with a weight function that, for any given clause, is strictly monotone with respect to the timestamp, so that older copies of a clause are preferred to newer ones:

locale weighted_FO_resolution_prover = FO_resolution_prover + fixes weight :: ′ a wclause ⇒ nat assumes i < j = ■ ⇒ weight (C, i) < weight (C, j)
The weight function is otherwise arbitrary. This gives nearly unlimited freedom when selecting clauses, which is possibly the most crucial heuristic in modern provers [START_REF] Schulz | Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving[END_REF]. For example, breadth-first search corresponds to the instance where weight (C, i) is defined as i.

The RP w prover uses ′ a wclause for clauses. It is defined inductively as follows:

inductive w :: ′ a wstate ⇒ ′ a wstate ⇒ bool where Neg A ∈ C ∧ Pos A ∈ C = ■ ⇒ (N ⊎ {(C, i)}, P, O, t) w1 (N , P, O, t) | D ∈ fst ' (P ⊎ O) ∧ subsumes D C = ■ ⇒ (N + {(C, i)}, P, O, t) w2 (N , P, O, t) | D ∈ fst ' N ∧ C ∈ fst ' P ∧ strictly_subsumes D C = ■ ⇒ (N , P, O, t) w3 (N , {(E, k) ∈ P . E C}, O, t) | D ∈ fst ' N ∧ strictly_subsumes D C = ■ ⇒ (N , P, O ⊎ {(C, i)}, t) w4 (N , P, O, t) | D ∈ fst ' (P ⊎ O) ∧ reduces D C L = ■ ⇒ (N ⊎{(C ⊎{L}, i)}, P, O, t) w5 (N ⊎{(C, i)}, P, O, t) | D ∈ fst ' N ∧ reduces D C L ∧ (∀j. (C ⊎ {L}, j) ∈ P = ■ ⇒ j ≤ i) = ■ ⇒ (N , P ⊎{(C ⊎{L}, i)}, O, t) w6 (N , P ⊎{(C, i)}, O, t) | D ∈ fst ' N ∧ reduces D C L = ■ ⇒ (N , P, O⊎{(C ⊎{L}, i)}, t) w7 (N , P ⊎{(C, i)}, O, t) | (N ⊎ {(C, i)}, P, O, t) w8 (N , P ⊎ {(C, i)}, O, t) | (∀(D, j) ∈ P . weight (C, i) ≤ weight (D, j)) ∧ N = mset_set ((λD. (D, t)) ' concl_of ' infers_between (set_mset (fst ' O)) C) = ■ ⇒ (∅, P ⊎ {(C, i)}, O, t) w9 (N , {(D, j) ∈ P . D C}, O ⊎ {(C, i)}, t + 1)
where fst is the function that returns the first component of a pair, mset_set converts a set to the multiset with exactly one copy of each element in the set, and set_mset converts a multiset to the set of elements in the multiset.

The most important differences with RP are in the last transition rule. This rule, which computes inferences, assigns timestamp t to each newly computed clause D and increments t. Moreover, since we want P to work as a priority queue, RP w chooses a clause C with the smallest weight.

Another difference is that RP w uses finite multisets for representing N , P, and O. They offer a compromise between sets in layer 1 and lists in layer 3. Finite multisets also help eliminate some unfair derivations. Finiteness guarantees that each clause in N gets the opportunity to move to P (and further to O). Moreover, whereas the set-based RP allows idle transitions, such as (N ∪{C}, P, O)

(N , P ∪{C}, O) for C ∈ N ∩ P, the use of multisets and ⊎ precludes such transitions in RP w .

Timestamps are preserved when clauses are moved between N , P, and O. They are also preserved by reduction steps (rules 5 to 7). This works because reduction can only take place finitely many times-a k-literal clause can be reduced at most k times. Therefore, there is no risk of divergence due to an infinite chain of reductions.

Timestamps introduce a new danger. It may be the case that a clause C is in the limit if we project away the timestamps, but that no single timestamped clause (C, i) belongs to the limit because the timestamps keep changing, as in the infinite sequence {(C, 0)}, {(C, 1)}, {(C, 2)}, . . . . This could in principle arise due to subsumption, leading to derivations such as the following:

(_, _ ⊎ {(C, 0)}, _) w (_, _ ⊎ {(C, 0), (C, 1)}, _) w (_, _ ⊎ {(C, 1)}, _) + w (_, _ ⊎ {(C, 1), (C, 2)}, _) w (_, _ ⊎ {(C, 2)}, _) + w • • • To prevent
this, the RP w rules are formulated so that whenever they remove the earliest copy of any clause C ∈ P, they also remove all its copies from P . This property is captured by the following lemma:

lemma preserve_min_P: S w S ′ ∧ (C, i) ∈ P_of S ∧ C ∈ fst ' P_of S ′ ∧ (∀k. (C, k) ∈ P_of S = ■ ⇒ k ≥ i) = ■ ⇒ (C, i) ∈ P_of S ′
This completes our review of RP w . As an intermediate step towards a more concrete prover, we restrict the weight function to be a linear equation that considers both timestamps and clause sizes: It is easy to prove that this definition of weight is strictly monotone and hence that this locale is a sublocale of weighted_FO_resolution_prover. This gives us a correspondingly specialized version of RP w that will form the basis of further refinement steps.

The idea of organizing P as a priority queue is well known in the automated reasoning community. Bachmair and Ganzinger [2, p. 44] mention it in a footnote, but they require the weight to be monotone not only in the timestamp but also in the clause size, claiming that this is necessary to ensure fairness. Our proof reveals that clause size is irrelevant, even in the presence of reductions. This demonstrates how working out the details and making all assumptions explicit using a proof assistant can help clarify fine theoretical points.

Refinement Proofs. To lift the soundness and completeness results about RP to RP w , we must first show that any possible behavior of RP w on states of type wstate is a possible behavior of RP on the corresponding values of type state:

lemma weighted_RP_imp_RP: S w S ′ = ■ ⇒ state_of S state_of S ′
The proof is by induction on the rules of RP w , with one difficult case. Inference computation (rule 9) converts a set to a finite multiset using mset_set, which is undefined for infinite sets. Thus, we must show only a finite set of inferences may be performed from a finite clause set: Soundness and Completeness Proofs. Using the refinement lemma weighted_RP_imp_RP, it is easy to lift the RP_ model theorem (Section 3) to RP w : theorem weighted_RP_model:

S w S ′ = ■ ⇒ (I | = grounding_of S ′ ⇐ ⇒ I | = grounding_of S)
Completeness is considerably more difficult. We first show that the use of timestamps ensures that all full RP w derivations are fair. In principle, a full derivation could be unfair by virtue of being finite and ending in a state such as N or P is nonempty. However, this is impossible because a transition of rule 8 or 9 could then be taken from the last state, contradicting the hypothesis that the derivation is full. Hence, finite full derivations are necessarily fair: lemma fair_if _finite: lfinite Ss = ■ ⇒ fair (lmap state_of Ss) There are two ways in which an infinite derivation Ss in RP w could be unfair: A clause could get stuck forever in N , or in P . We show that the N case is impossible by defining a measure on states that decreases with respect to the lexicographic extension of > on nat to pairs:

abbreviation RP_basic_measure :: ′ a wstate ⇒ nat 2 where RP_basic_measure (N , P, O, t) ≡ sum ((λ(C, _). |C | + 1) ' (N ⊎ P ⊎ O)), |N | The first component of the pair is the total size of all the clauses in the state, plus 1 for each clause to ensure that empty clauses are also counted. The second component is the number of clauses in N. It is easy to see why the measure is decreasing. Rule 9, inference computation, is not applicable due to our assumption that a clause remains stuck in N . Rule 8, which moves a clause from N to P, decreases the measure's second component while leaving the first component unchanged. The other rules decrease the first component since they remove clauses or literals. Formally:

lemma weighted_RP_basic_measure_decreasing_N : S w S ′ ∧ (C, _) ∈ N_of S = ■ ⇒ (RP_basic_measure S ′ , RP_basic_measure S) ∈ RP_basic_rel where RP_basic_rel = natLess <lex> natLess and natLess = {(m, n) | m < n}.
What if a clause C is stuck in P? Lemma preserve_min_P states that in any step, either all copies of C are removed or the one with the lowest timestamp is kept. Hence, C's timestamp will either remain stable or decrease over time. Since > is well founded on natural numbers, eventually a fixed i will be reached and will belong to the limit:

lemma persistent_wclause_in_P_if _persistent_clause: C ∈ Liminf (lmap P_of (lmap state_of Ss)) = ■ ⇒ ∃i. (C, i) ∈ Liminf (lmap (set_mset • P_of) Ss)
Again, we define a measure, but it must also decrease when inferences are computed and new clauses appear in N . (In this case, RP_basic_measure may increase.) Our new measure is parameterized by a predicate p that can be used to filter out undesirable clauses: abbreviation RP_filtered_measure ::

( ′ a wclause ⇒ bool) ⇒ ′ a wstate ⇒ nat 3 where RP_filtered_measure p (N , P, O, t) ≡ sum ((λ(C, _). |C | + 1) ' {Di ∈ N ⊎ P ⊎ O | p Di}), |{Di ∈ N | p Di}| , |{Di ∈ P | p Di}|
Notice that the case RP_filtered_measure (λ_. True) essentially amounts to RP_basic_measure. In the formalization, we use RP_filtered_measure (λ_. True) to avoid duplication.

Suppose the clause C that is stuck in P has weight w in the limit, and suppose that a clause D is moved from P to O by rule 9. That clause's weight must be at most w; otherwise, it would not have been preferred to C. Thus, infinite derivations necessarily consist of segments each consisting of finitely many applications of rules other than rule 9 followed by an application of rule 9: ( * w1-8 • w9 ) ω . Since each application of rule 9 increases the t component of the state, eventually we reach a state in which t > w. As a consequence of strict monotonicity of weight, any clauses generated by inference computation from that point on will have weights above C's, and if C remains stuck, then so must these clauses. Thus, we can ignore these clauses altogether, by using λ(C, i). i ≤ w as the filter p. We adapt the corresponding relation to consider the extra argument: abbreviation RP_filtered_rel :: (nat 3 ) 2 set where RP_filtered_rel ≡ natLess <lex> natLess <lex> natLess

The measure RP_filtered_measure (λ(_, i). i ≤ w) decreases for steps occurring between inference computations and for all steps once we have reached a state where t > w (at which point all inference computations are blocked by C).

To obtain a measure that also decreases on inference computation, we add a component w + 1 -t to the measure. We also add a component RP_basic_measure S to ensure that the measure decreases when a clause (C, i) such that i > w is simplified. This yields the combined measure abbreviation RP_combined_measure :: The function should be invoked with N as the input problem, P = O = ∅, and an arbitrary timestamp t (e.g., 0). The loop is loosely modeled after Vampire's proof procedure [START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF].

nat ⇒ ′ a wstate ⇒ nat × nat 3 × nat 3 where RP_combined_measure w S ≡ (w + 1 -t_of S, RP_filtered_measure (λ(_, i). i ≤ w) S, RP_basic_measure S)
In Isabelle, the list-based representations compel us to introduce the following type abbreviations:

type_synonym ′ a lclause = ′ a literal list type_synonym ′ a dclause = ′ a lclause × nat type_synonym ′ a dstate = ′ a dclause list × ′ a dclause list × ′ a dclause list × nat
The prover is defined inside a locale that inherits weighted_ FO_resolution_prover_with_size_timestamp_factors. The core function, RP d _step, performs a single iteration of the main loop. Here is the definition, excluding auxiliary functions:

fun RP d _step :: ′ a dstate ⇒ ′ a dstate where RP d _step (N , P, O, t) = if ∃Ci ∈ P @ O. fst Ci = [] then ([], [], remdups P @ O, t + |remdups P |) else case N of [] ⇒ (case P of [] ⇒ (N , P, O, t) | P 0 # P ′ ⇒ let (C, i) = select_min_weight_clause P 0 P ′ ; N = map (λD. (D, t)) (remdups (resolve_rename C C @ concat (map (resolve_rename_both_ways C •fst) O))); P = filter (λ(D, j). mset D mset C) P; O = (C, i) # O; t = t + 1 in (N , P, O, t)) | (C, i) # N ⇒ let C = reduce (map fst (P @ O)) [] C in if C = [] then ([], [], [([], i)], t + 1) else if is_tautology C ∨ subsume (map fst (P @ O)) C then (N , P, O, t) else let P = reduce_all C P; (back_to_P, O) = reduce_all2 C O; P = back_to_P @ P; O = filter ((¬) • strictly_subsume C • fst) O; P = filter ((¬) • strictly_subsume C • fst) P; P = (C, i) # P in (N , P, O, t)
The # operator abbreviates the Cons constructor, and @ is the append operator.

The existential quantifier above is unproblematic because it ranges over a finite set, but some of the auxiliary functions use infinite quantification. Notably, subsumption of a clause D by another clause C is defined as ∃σ. C • σ ⊆ D (Section 2), where σ ranges over substitutions. Nonexecutable constructs are acceptable if we know that we can replace them by equivalent executable constructs further down the refinement chain; for example, an implementation of subsumption can compute a witness σ using matching, instead of blindly enumerating all possible substitutions.

The Since the recursion may diverge, we cannot introduce the function using the fun command [START_REF] Krauss | Partial Recursive Functions in Higher-Order Logic[END_REF]. Instead, we use par-tial_function (option) [START_REF] Krauss | Recursive Definitions of Monadic Functions[END_REF], which puts the computation in an option monad. The function's result is of the form Some R if the recursion terminates and None otherwise. O ′ , t + |remdups P ′ |) for P ′ = filter (λ(D, j). mset D mset C) P, O ′ = remdups P ′ @ O, and suitable N ′ and (C, i) ∈ P . The last step is justified by the induction hypothesis.

Refinement

case N = P = []:

Contradiction with the assumption that (N , P, O, t) is a nonfinal state.

case N = []:

It suffices to show that the transition wstate_of ([], P, O, t)

w9 wstate_of (N ′ , P ′ , (C, i) # O, t + 1) is possible, where (C, i) ∈ P is a minimal-weight clause, N ′ = map (λD. (D, t)) (remdups (resolve_rename C C @ concat (map (resolve_rename_both_ways C • fst) O))), and P ′ = filter (λ(D, j). mset D mset C) P. The main proof obligation is that N ′ , converted to multisets, equals the multiset mset_set ((λD. (D, t)) ' concl_of ' infers_between (set_mset (fst ' O)) C) specified in rule w9 . The distance between the functional program and its mathematical specification is at its greatest here. The proof is tedious but straightforward.

otherwise:

Let

C ′ = reduce (map fst P @ map fst O) [] C. If C ′ = [], then wstate_of ((C, i) # N ′ , P, O, t) * w5 wstate_of (([], i) # N ′ , P, O, t) * w3 wstate_of (([], i) # N ′ , [], O, t) * w4 wstate_of (([], i) # N ′ , [], [], t) w8 wstate_of (N ′ , [([], i)], [], t) * w2 wstate_of ([], [([], i)], [], t) w9 wstate_of ([], [], [([], i)], t) Otherwise, if is_tautology C ′ ∨ subsume (map fst (P@ O)) C ′ , then wstate_of ((C, i) # N , P, O, t) * w5 wstate_of ((C ′ , i) # N , P, O, t) w1,2 wstate_of (N , P, O, t) Otherwise: wstate_of ((C, i) # N ′ , P, O, t) * w5 wstate_of ((C ′ , i) # N ′ , P, O, t) * w6 wstate_of ((C ′ , i) # N ′ , P ′ , O, t) * w7 wstate_of ((C ′ , i) # N ′ , back_to_P @ P ′ , O ′ , t) * w4 wstate_of ((C ′ , i) # N ′ , back_to_P @ P ′ , O ′′ , t) * w3 wstate_of ((C ′ , i) # N ′ , P ′′ , O ′′ , t) w8 wstate_of (N ′ , (C ′ , i) # P ′′ , O ′′ , t)
for suitable lists P ′ , back_to_P, O ′ , O ′′ , and P ′′ .

Soundness and Completeness Proofs. Let S 0 = (N 0 , [], [], t 0 ) be an arbitrary initial state. Soundness means that whenever RP d S 0 terminates with some clause set R, then R is a saturation that satisfies the same models as N 0 . Moreover, if N 0 is unsatisfiable, then R contains ⊥, providing a simple syntactic check for unsatisfiability. Completeness means that divergence is possible only if N 0 is satisfiable. For satisfiable clause sets N 0 , both termination and divergence are possible.

To lift soundness and completeness results from RP w to RP d , we first define Ss as a full chain of nontrivial RP d steps starting from S 0 . We let Ss = derivation_from S 0 , with primcorec derivation_from :: ′ a dstate ⇒ ′ a dstate llist where derivation_from S = LCons S (if is_final S then LNil else derivation_from (RP d _step S)) Based on Ss, we let wSs = lmap wstate_of Ss and note that wSs is a full chain of "big" + w steps. Using a lemma that will be proved below, we obtain a full chain sswSs of "small" w steps. This chain satisfies the conditions postulated on Ss in Section 4, allowing us to lift the results presented there.

The soundness results are proved in a nameless locale, or context, that assumes termination of RP d : fixes R :: ′ a lclause list assumes RP d S 0 = Some R The definition of RP d , using partial_function, gives us an induction rule restricted to the case where RP d terminates (i.e., returns a Some value). This rule can be used to prove that Ss and hence wSs and sswSs are finite sequences.

Soundness takes the form of a pair of theorems that lift weighted_RP_model and weighted_RP_saturated:

theorem deterministic_RP_model: I | = grounding_of N 0 ⇐ ⇒ I | = grounding_of R theorem deterministic_RP_saturated: saturated_upto (grounding_of R)
In most applications, all that matters is the satisfiability status of the set N 0 . It can be retrieved syntactically:

corollary deterministic_RP_refutation: ¬ satisfiable (grounding_of N 0 ) ⇐ ⇒ ∅ ∈ R
Completeness is proved in a separate context that assumes nontermination: RP d S 0 = None. The strongest result we prove is that this assumption implies the satisfiability of N 0 :

theorem deterministic_RP_complete: satisfiable (grounding_of N 0 )
The proof is by contradiction:

Assume that ¬ satisfiable (grounded_of N 0 ). Hence, by weighted_RP_complete we have ∅ ∈ O_of sswSs. It is easy to show that sswSs's limit is a subset of wSs's limit; hence ∅ ∈ O_of wSs. This implies the existence of a natural number k such that ∅ ∈ O_of (lnth wSs k). Hence ∅ ∈ O_of (RP d _step k S 0 ). However, by an induction on k, we can show that RP d must terminate after at most k iterations, contradicting the assumption that RP d diverges.

A Coinductive Puzzle. A single "big" step of the deterministic prover RP d may correspond to many "small" steps of the weighted prover RP w . To transfer the results from RP w to RP d , we must expand the big steps. The core of the expansion is an abstract property of chains and transitive closure:

Let R be a relation and xs a chain of R + transitions. There exists a chain of R transitions that embeds xs -i.e., that contains all elements of xs in the same order and with only finitely many elements inserted between each pair of consecutive elements of xs.

On finite chains, this property can be proved by straightforward induction. But the completeness proof must also consider infinite chains. Coinduction and corecursion up-to techniques are useful for such tasks.

The desired property is stated formally as follows:

lemma chain_tranclp_imp_exists_chain: chain R + xs = ■ ⇒ ∃ys. chain R ys ∧ xs ⊑ ys ∧ lhd xs = lhd ys ∧ llast xs = llast ys
where the embedding ⊑ of lazy lists is defined coinductively using + +, which prepends a finite list to a lazy list: The definition of ⊑ ensures that infinite lazy lists only embed other infinite lazy lists, but not the finite ones: xs ⊑ ys = ■ ⇒ (lfinite xs ⇐ ⇒ lfinite ys). The unguarded calls to llast may seem worrying, but the function is conveniently defined to always return the same unspecified element for infinite lists.

To prove the lemma above, we instantiate the existential quantifier by the following corecursively defined witness:

corec wit :: ( ′ a ⇒ ′ a ⇒ bool) ⇒ ′ a llist ⇒ ′ a llist where wit R xs = (case xs of LCons x (LCons y ys) ⇒ LCons x (pick R x y + + wit R (LCons y ys)) | _ ⇒ xs)
Here pick R x y returns an arbitrary finite list of R-related states connecting the R + -related x and y. Its definition is pick R x y = (SOME zs. chain R (llist_of (x # zs @ [y]))), where llist_of converts finite lists into lazy lists and SOME is Hilbert's choice operator. Thus, pick satisfies the characteristic property R + x y = ■ ⇒ chain R (llist_of (x # pick R x y @ [y])). The nonexecutability entailed by the use of Hilbert choice is unproblematic because the wit function is used only in the proofs and not in the prover's code.

The definition of wit is not primitively corecursive. Although there is a guarding LCons constructor, the corecursive call occurs under + +, which makes the productivity of this function nontrivial. This syntactic structure of the definition is called corecursive up to + +. Ultimately, wit is productive because + + does not remove any LCons constructors from its second arguments. A slightly weaker requirement, called friendliness, is supported by Isabelle's corec command [START_REF] Christian Blanchette | Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants[END_REF]. For the above definition to be accepted + + must be registered as a "friend. " This involves a one-line proof.

The four conjuncts in chain_tranclp_imp_exists_chain are discharged in turn under the assumption chain R + xs. In order of increasing difficulty: lhd (wit R xs) = lhd xs follows by simple rewriting. Next, llast (wit R xs) = llast xs requires an induction in the case of finite chains xs. For any infinite chain zs, llast zs is defined as a fixed unspecified ′ a value. The properties xs ⊑ wit R xs and chain R (wit R xs) require a coinduction on ⊑ and chain, respectively. In keeping with the definition, plain coinduction on ⊑ and chain does not suffice, and we must use coinduction up to ++ on ⊑ and chain.

The property chain_tranclp_imp_exists_chain easily extends to full chains.

Obtaining Executable Code

Our deterministic prover RP d is already quite close to being an executable program. The fourth refinement, the prover RP x , adds the missing ingredients: a concrete representation of terms and an executable algorithm for clause subsumption.

First-Order Terms. We instantiate our abstract notion of atom using a particularly comprehensive formalization of terms developed as part of the IsaFoR library [START_REF] Thiemann | Certification of Termination Proofs using CeTA[END_REF]. This rewriting-independent part of IsaFoR has recently moved to the Archive of Formal Proofs [START_REF] Sternagel | First-Order Terms[END_REF].

IsaFoR terms are defined as the following datatype:

datatype ( ′ f , ′ v) term = Var ′ v | Fun ′ f (( ′ f , ′ v) term list)
To simplify notation, in this paper we fix ′ f = ′ v = nat and abbreviate ( ′ f , ′ v) term by term. In the formalization, polymorphic types are used whenever possible. IsaFoR also defines the standard monadic term substitution • :: term ⇒ ( ′ v ⇒ term) ⇒ term and a unify :: (term × term) list ⇒ lsubst ⇒ lsubst function, where lsubst = ( ′ v × term) list is the list-based representation of a finite substitution. The function unify computes the MGU for a list of unification constraints that is compatible with a given substitution. IsaFoR includes a wealth of theorems, including the correctness of unify and the well-foundedness of strict term generalization, defined as (∃σ . s

• σ = t) ∧ ( σ . t • σ = s).
This infrastructure allows us to conveniently instantiate our locales substitution_ops, substitution, and mgu. We instantiate the type ′ a of atoms with term and the type ′ s of substitutions with ′ v ⇒ term and the constants •, id, •, and atm_of_atms with •, Var, λσ τ x . σ x • τ , and (arbitrarily) Fun 0. For the MGU computation, there is a slight type mismatch: IsaFoR offers a list-based unifier, whereas our locale requires the type term set set ⇒ ( ′ v ⇒ term) option. It is easy to translate a finite set of finite sets of terms into a finite list of pairs of constraints. To be executable, the translation requires us to sort the terms belonging to set with respect to an arbitrary (but executable) linear order.

Only the function renamings_apart was not present in IsaFoR. We supply a definition:

fun renamings_apart :: term clause list ⇒ ( ′ v ⇒ term) list where renamings_apart [] = [] | renamings_apart (C # Cs) = let σs = renamings_apart Cs in (λv. v + max ({0} ∪ vars_clause_list (Cs • σs)) + 1) # σs
where vars_clause_list :: term clause list ⇒ ′ v set returns the variables contained in a list of clauses. The creation of fresh variable names relies on ′ v = nat.

Finally, the FO_resolution_prover locale requires that the type of atoms supports two comparison operators: a wellorder > and a comparison ≻ that is stable under substitution

(i.e., B ≻ A = ■ ⇒ B • σ ≻ A • σ ).
Moreover, > and ≻ must coincide on ground atoms. We instantiate ≻ with the Knuth-Bendix order [START_REF] Knuth | Simple Word Problems in Universal Algebras[END_REF] on terms, provided by IsaFoR [START_REF] Sternagel | Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion[END_REF]. This order is executable, stable under substitution, well founded, and total on ground terms. The well-order >, which must be total on all terms, is then defined as an arbitrary extension of a partial well-founded order ≻ to a well-order, using Hilbert choice. This makes > nonexecutable, but this is acceptable since it is ≻, not >, that is used in the prover's code.

Clause Subsumption. The second hurdle concerns clause subsumption. Its mathematical definition, subsumes C D ⇐ ⇒ ∃σ. C • σ ⊆ D, involves an infinite quantification.

The problem of deciding whether such a substitution exists is NP-complete [START_REF] Kapur | NP-Completeness of the Set Unification and Matching Problems[END_REF]. We start with the following naive code. In contrast to the mathematical definition, which operates on multisets of literals, our function operates on lists:

fun subsumes_list :: term literal list ⇒ term literal list ⇒ ( ′ v ⇒ term option) ⇒ bool where subsumes_list [] Ks σ = True | subsumes_list (L # Ls) Ks σ = (∃K ∈ set Ks. is_pos K = is_pos L ∧ case match_term_list [(atm_of L, atm_of K)] σ of None ⇒ False | Some ρ ⇒ subsumes_list Ls (remove1 K Ks) ρ)
In the Cons case, we must consider all possible matching literals for L from Ks compatible with the substitution σ . The bounded existential quantification that expresses this nondeterminism can be executed by iterating over the finite list Ks. The functions is_pos and atm_of are the discriminator and selector for literals. The function match_term_list is provided by IsaFoR. It attempts to extend a given substitution into Some matcher for a list of matching constraints, given as term pairs. If the extension is impossible, match_term_list returns None. This substitution-passing style is typical of purely functional implementations of matching.

It is easy to prove that the above executable function implements clause subsumption: subsumes (mset Ls) (mset Ks) = subsumes_list Ls Ks (λx . None), where mset converts lists to multisets by forgetting the order of the elements. After the registration of this equation, Isabelle's code generator will rewrite any code that contains the nonexecutable left-hand side to use the executable right-hand side instead.

Clause subsumption is a hot spot in a resolution prover [START_REF] Schulz | Simple and Efficient Clause Subsumption with Feature Vector Indexing[END_REF]. Following Tammet [START_REF] Tammet | Towards Efficient Subsumption[END_REF], we implement a heuristic that often reduces the number of calls to match_term_list, which is linear in the size of the input terms, by first performing a simpler, imprecise comparison. For example, terms with different root symbols will never match, and these can be compared in constant time. Similarly, literals with opposite polarities cannot match. We sort our (list-represented) clauses with respect to a literal quasi-order (i.e., a transitive and reflexive relation) leq_lit such that leq_lit L K only if is_pos L = is_pos K and match_term_list [(atm_of L, atm_of K)] σ = Some ρ for some σ and ρ. Any quasi-order satisfying this property can be used in a refinement of subsumes_list to remove too small literals (with respect to leq_lit), as highlighted in gray below: fun subsumes_list ′ ::

term literal list ⇒ term literal list ⇒ ( ′ v ⇒ term option) ⇒ bool where subsumes_list ′ [] Ks σ = True | subsumes_list ′ (L # Ls) Ks σ = let Ks = filter (leq_lit L) Ks in (∃K ∈ set Ks. is_pos K = is_pos L ∧ case match_term_list [(atm_of L, atm_of K)] σ of None ⇒ False | Some ρ ⇒ subsumes_list ′ Ls (remove1 K Ks) ρ)
The lemma subsumes_list Ls Ks ρ = subsumes_list ′ (sort leq_lit Ls) Ks ρ allows the code generator to refine the original version. In RP x , we let leq_lit be a quasi-order that (1) considers negative literals smaller than positive ones; (2) considers variables smaller than nonvariables; and (3) sorts atoms according to a total order on their root symbols.

This refinement is a local optimization: It requires us to explicitly sort one of the input clauses. A potentially more efficient refinement would be to ensure that all clauses in the prover's state are sorted with respect to leq_lit. Sorting Ls at each invocation of subsumption could then be avoided, and filtering Ks could be performed more efficiently. However, maintaining the invariant would require changes throughout the prover's code.

The End Result. Finally, Isabelle can export our prover to Standard ML, Haskell, OCaml, or Scala. The command export_code RP x in SML module_name RP generates an ML module containing the implementation of our prover in about 1000 lines of code, including dependencies. The generated module exports the function RPx : (term literal list * nat) list -> bool. The input is the N component of an initial state, which consists of pairs of clauses and arbitrary timestamps (e.g., 0).

Even though in Isabelle we have proved that for any unsatisfiable input RP x will terminate and return False, the code generator guarantees only partial correctness of its output: If the ML program terminates on the ML input generated from the Isabelle term t and evaluates to the Boolean result b, the proposition RP x t = b is provable in Isabelle; by soundness, b indicates the satisfiability of the input clause set. There is recent work towards providing stronger guarantees and reducing the generator's trusted code base [START_REF] Hupel | A Verified Compiler from Isabelle/HOL to CakeML[END_REF].

Empirical Evaluation. To measure the gap with the state of the art, we compare our prover's performance with that of three other provers on a benchmark suite. TPTP (Thousands of Problems for Theorem Provers) [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure: From CNF to TH0, TPTP v6.4.0[END_REF] is the de facto standard library for benchmarking automatic provers. We extended RP x with the trusted TPTP parser from Metis [START_REF] Hurd | First-Order Proof Tactics in Higher-Order Logic Theorem Provers[END_REF]. We benchmarked E 2.1, Vampire 4.2.2, Metis 2.4, and RP x on 1000 randomly selected equality-free problems from the TPTP's FOF (first-order formulas) and CNF (first-order formulas in conjunctive normal form) categories. We converted all FOF problems to CNF using E's clausifier. Each prover was run on each problem for 60 s on an Intel Core i9-7900X (3.3 GHz 10-Core) with 128 GB of RAM.

The results are summarized in the following The detailed results of the evaluation are available online, together with instructions for reproducing them. 3As expected, RP x is not competitive. A prover's performance comes from its calculus, its heuristics, and its indexing data structures. RP x employs an excellent calculus but mediocre heuristics and data structures. Better performance could be achieved by working on these last two aspects. Heuristics are often easy to verify, because their inputoutput specifications are permissive, but formalizing optimized data structures can be very laborious [START_REF] Fleury | A Verified SAT Solver with Watched Literals using Imperative HOL[END_REF].

Nevertheless, sometimes the calculus is all that matters. Benchmark MSC015 from the TPTP library is a particularly challenging family Φ n of first-order problems, each consisting of the following n + 2 clauses: . . .

¬ p(x 1 , . . . , x n-2 , a, b) ∨ p(x 1 , . . . , x n-2 , b, a) ¬ p(x 1 , . . . , x n-2 , x n-1 , a) ∨ p(x 1 , . . . , x n-2 , x n-1 , b)
A comment in the benchmark warns us that back in 2007, no prover could solve the Φ 23 within an hour. Even in 2018, only one prover solves Φ 22 within 300 s, and four provers solve Φ 20 within 300 s. RP x solves Φ 20 in 100 s and Φ 22 in 200 s. Presumably, the reason for this success is that RP x fortuitously chooses an instance of the Knuth-Bendix order that is well suited to this benchmark.

Discussion and Related Work

We found Bachmair and Ganzinger's [START_REF] Bachmair | Resolution Theorem Proving[END_REF] chapter and its formalization [START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's Ordered Resolution Prover[END_REF][START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover[END_REF] suitable as a starting point for a verified prover. Nonetheless, we faced some difficulties, notably concerning the identification of suitable refinement layers. We developed layers 2, 3, and 4 largely in parallel, with each of the authors working on a separate layer. Bringing layer 2 into a state such that it both ensures fairness and could be refined further by layer 3 required several iterations.

Stepwise refinement helped us achieve separation of concerns: fairness, determinism, and executability were achieved successively. Another strength of this methodology is that it allows us to prove results at a high level of abstraction; for example, fairness is established at layer 2 already and is inherited by subsequent layers. The main difficulty with refinement is that some nontrivial machinery is necessary to lift results from one layer to the next. We believe the gain in modularity makes this worthwhile.

It took us quite some time to design a suitable measure to prove the fairness of the layer 2 prover RP w . Our solution amounts to advancing to a state carrying a suitably high timestamp and filtering out all overly heavy clauses. Initially, our proof consisted of two steps-advancing and filteringeach with its own measure. This proof gave us the assurance that RP w was fair, but we found that combining the measures is both more succinct and more intelligible.

Our main objective was not to reach qed as quickly as possible but rather to investigate how to harness a modern proof assistant to formalize the metatheory of automatic theorem provers. We found Isabelle suitable for this verification task. The Isar proof language allows us to state key intermediate steps, as in a paper proof. Standard tactics, including Isabelle's simplifier, can be used to discharge proof obligations. The Sledgehammer tool [START_REF] Paulson | Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers[END_REF] employs superposition provers and SMT (satisfiability modulo theories) solvers to swiftly identify which lemmas can be used to prove a goal; standard Isabelle tactics are then used to reconstruct the proof. Isabelle's support for coinductive methods, including the coinductive, codatatype, and corec commands, helps us reason about infinite processes. Locales are a useful abstraction for defining the refinement layers. And Isabelle's libraries, the Archive of Formal Proofs, and IsaFoR certainly saved us months of labor.

The Archive also includes a refinement framework [START_REF] Lammich | Automatic Data Refinement[END_REF], which has been used in a separate effort to connect the imperative code of an efficient SAT solver to an abstract calculus [START_REF] Christian Blanchette | A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality[END_REF]. The framework is helpful in a variety of situations, including when the refinement relation between a concrete and an abstract data representation is not a function. But since converting a list to a multiset (between our levels 3 and 2) or a multiset to a set (between levels 2 and 1) is a function, we did not see a need to employ it. Moreover, the framework is currently not designed for refining semidecision procedures, as acknowledged privately by its developer. We conjecture that its support for separation logic could be useful if we were to refine the prover further to obtain imperative code.

Thanks to the verification, we can trust to a very high extent that our ordered resolution prover is sound and complete. To make the prover's performance competitive with E, SPASS, and Vampire, we would need to extend the current work along two axes. First, we should use superposition, together with its extensive simplification machinery, as the base calculus. A good starting point would be to apply our methodology to Peltier's [START_REF] Peltier | A Variant of the Superposition Calculus[END_REF] formalization of superposition. Given that a large part of a modern superposition prover's code consists of heuristics, which are easy to verify, the full verification of a competitive superposition prover appears to be a realistic objective for a forthcoming Ph.D. thesis. Second, the refinement chain should be continued to cover optimized algorithms and data structures. These could be specified by refining layer 4 further, along the lines of Fleury et al.'s [START_REF] Fleury | A Verified SAT Solver with Watched Literals using Imperative HOL[END_REF] refinement of an imperative SAT solver.

In computer science, a metatheory may inspire an implementation, or vice versa, but the connection is seldom made explicit. By formalizing the metatheory, the implementation, and their connection, we can demonstrate not only the implementation's correctness but also the metatheory's adequacy for describing potential implementations. In particular, we have now confirmed that Bachmair and Ganzinger [START_REF] Bachmair | Resolution Theorem Proving[END_REF] accurately describe the abstract principles of an executable functional prover (with a few exceptions [START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover[END_REF]), even though they provide few details beyond layer 1.

We built the prover on our earlier formalization [START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's Ordered Resolution Prover[END_REF][START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover[END_REF] of ordered resolution. Related efforts developed using Isabelle/ HOL include Peltier's [START_REF] Peltier | A Variant of the Superposition Calculus[END_REF] formalization of superposition and Schlichtkrull's [START_REF] Schlichtkrull | Formalization of the Resolution Calculus for First-Order Logic[END_REF] formalization of unordered resolution. These developments cover only logical calculi; had we started with any of them, the first step would have been to define an abstract prover in the style of layer 1 and prove basic properties about it. Another related effort is Hirokawa et al.'s [START_REF] Hirokawa | Infinite Runs in Abstract Completion[END_REF] formalization of ordered completion, which (like ordered resolution) can be regarded as a special case of superposition.

Formalizing a theorem proving tool using a theorem proving tool is a thrilling (if self-referential) prospect for many researchers. An early result is Ridge and Margetson's [START_REF] Ridge | A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic[END_REF] verified first-order prover, based on a sequent calculus for first-order logic without full first-order terms but only variables. Kumar et al. [START_REF] Kumar | Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation[END_REF] formalized the soundness of a proof assistant for higher-order logic. Jensen et al. [START_REF] Birch Jensen | Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL[END_REF] verified the soundness of a kernel for a proof assistant for first-order logic that includes a tableau prover. There are several verified SAT solvers [6, 27-29, 31, 44]. SAT being a decidable problem, termination has been proved for most solvers. First-order logic, on the other hand, is semidecidable.

A pragmatic approach to combining the efficiency of unverified code with the trustworthiness of verified code involves checking certificates produced by reasoning tools-e.g., proofs produced by SAT solvers [START_REF] Cruz-Filipe | Efficient Certified RAT Verification[END_REF][START_REF] Lammich | The GRAT Tool Chain-Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees[END_REF]. Researchers from the first-order theorem proving community are now advocating this approach for their systems [START_REF] Reger | Checkable Proofs for First-Order Theorem Proving[END_REF]. An ad hoc version of this approach is used in Sledgehammer and HOLy-Hammer to reconstruct proofs found by external automatic provers [START_REF] Christian Blanchette | Semi-intelligible Isar Proofs from Machine-Generated Proofs[END_REF][START_REF] Kaliszyk | PRocH: Proof Reconstruction for HOL Light[END_REF].

Conclusion

Starting from an abstract description of an ordered resolution prover [START_REF] Schlichtkrull | Formalization of Bachmair and Ganzinger's Ordered Resolution Prover[END_REF][START_REF] Schlichtkrull | Formalizing Bachmair and Ganzinger's Ordered Resolution Prover[END_REF], we verified, through a refinement chain, a purely functional prover that uses lists as its main data structure. The resulting program is interesting in its own right and could be refined further to obtain an implementation that is competitive with the state of the art.

Stepwise refinement is a keystone of our methodology, and we found it adequate. Each refinement step cleanly isolates concerns, yielding intelligible proof obligations. Refinement also helped us identify an unnecessary assumption in Bachmair and Ganzinger's [START_REF] Bachmair | Resolution Theorem Proving[END_REF] chapter and clarify the argument. Lifting results from one layer to another required some thought, especially the completeness results, which correspond to liveness properties.

Having now established a methodology and built basic formal libraries, we expect that verifying other provers, using Isabelle or other systems, will be substantially easier. Because it is based on Bachmair and Ganzinger's framework, our approach generally applies to all saturation-based provers, with or without redundancy. This includes resolution, paramodulation, ordered rewriting, superposition, and variants thereof, covering many of the most successful provers for equational [START_REF] Claessen | Efficient Encodings of First-Order Horn Formulas in Equational Logic[END_REF][START_REF] Hillenbrand | WALDMEISTER-High-Performance Equational Deduction[END_REF], first-order [START_REF] Kovács | First-Order Theorem Proving and Vampire[END_REF][START_REF] Schulz | System Description: E 1.8[END_REF][START_REF] Weidenbach | SPASS Version 3.5[END_REF], and higher-order logic [START_REF] Steen | The Higher-Order Prover Leo-III[END_REF].

  locale weighted_FO_resolution_prover_with_size_ timestamp_factors = FO_resolution_prover + fixes size_factor :: nat and timestamp_factor :: nat assumes timestamp_factor > 0 begin fun weight :: ′ a wclause ⇒ nat where weight (C, i) = size_factor * |C | + timestamp_factor * i end where |C | = A : A∈C ∨ ¬A∈C |A|.

  lemma finite_ord_FO_resolution_inferences_between: finite D = ■ ⇒ finite (infers_between D C) A binary resolution inference takes two premises, of the form CAA = C ∨ A 1 ∨ • • • ∨ A k and DA = ¬A ∨ D, and produces a conclusion E = (C ∨ D) • σ . It can be represented compactly by a tuple of the form (CAA, DA, AA, A, E), where AA = A 1 ∨ • • • ∨ A k . We must show that the set of such tuples produced by infers_between is finite, assuming D is finite. First, observe that the last component E of a tuple is determined by the other four. Hence it suffices to consider quadruples (CAA, DA, AA, A). Let DC = D ∪ {C}, and let n be the length of the longest clause in DC. Moreover, let A = D ∈DC atms_of D and AA = {B | set_mset B ⊆ A ∧ |B| ≤ n}. Then all inferences between D and C belong to DC × DC × AA × A, a cartesian product of finite sets.

  coinductive ⊑ :: ′ a llist ⇒ ′ a llist ⇒ bool where lfinite xs = ■ ⇒ LNil ⊑ xs | xs ⊑ ys = ■ ⇒ LCons x xs ⊑ zs + + LCons x ys fun + + :: ′ a list ⇒ ′ a llist ⇒ ′ a llist where [] + + xs = xs | (z # zs) + + xs = LCons z (zs + + xs)

¬

  p(b, . . . , b) p(a, . . . , a) ¬ p(a, b, . . . , b) ∨ p(b, a, . . . , a) ¬ p(x 1 , a, b, . . . , b) ∨ p(x 1 , b, a, . . . , a)

  This measure is indeed decreasing with respect to a leftto-right lexicographic order: lemma weighted_RP_basic_measure_decreasing_P:S w S ′ ∧ Ci ∈ P_of S = ■ ⇒ (RP_combined_measure (weight Ci) S ′ , RP_combined_measure (weight Ci) S) ∈ natLess <lex> RP_filtered_rel <lex> RP_basic_rel By combining the two lemmas weighted_RP_basic_measure_ decreasing_N and weighted_RP_basic_measure_decreasing_P, we can prove all derivations starting with P = O = ∅ fair: theorem weighted_RP_fair: fair (lmap state_of Ss) Since all derivations are fair and RP w derivations correspond to RP derivations, it is trivial to lift RP's saturation and completeness theorems: corollary weighted_RP_saturated: saturated_upto (Liminf (lmap grounding_of Ss)) corollary weighted_RP_complete: ¬ satisfiable (grounding_of (lhd Ss)) = ■ ⇒ ∅ ∈ O_of (Liminf (lmap state_of Ss)) The third refinement layer defines a functional program RP d that embodies a specific rule application strategy, thereby eliminating RP w 's nondeterminism. Clauses are represented by lists, and multisets of clauses by lists of lists.

	5 Eliminating Nondeterminism
	Definition. Our prover corresponds roughly to the follow-
	ing pseudocode:
	function RP if C = ⊥ then
	return {⊥}
	else if C is neither a tautology nor subsumed by
	a clause in P ⊎ O then
	reduce P using C;

d (N , P, O, t) is repeat forever if ⊥ ∈ P ⊎ O then return P ⊎ O else if N = P = ∅ then return O else if N = ∅ then let C be a minimal-weight clause in P; N := conclusions of all inferences from O ⊎ {C} involving C, with timestamp t; move C from P to O; t := t + 1 else remove an arbitrary clause C from N ; reduce C using P ⊎ O; reduce O using C, moving any reduced clauses from O to P; remove all clauses from P and O that are strictly subsumed by C; add C to P

  main program is a tail-recursive function that repeatedly calls RP d _step until a final state ([], [], O, t) is reached, at which point it returns the set O stripped of its timestamps: partial_function (option) RP d :: ′ a dstate ⇒ ′ a lclause list option where RP d S = if is_final S then Some (map fst (O_of S)) else RP d (RP d _step S)

  Proofs. Using refinement, we connect the RP d _ step function to the RP w predicate. RP d _step has a coarser granularity than RP w : A single invocation on a nonfinal state S can amount to a chain of RP w transitions. This is captured by the following (weak-)refinement property: lemma nonfinal_deterministic_RP_step: ¬ is_final S = ■ ⇒ wstate_of S + w wstate_of (RP d _step S) where wstate_of converts RP d states to RP w states. The entire proof, including key lemmas, is about 1300 lines long. It follows the case distinctions present in RP

d _step's definition: case ∃Ci ∈ P @ O. fst Ci = []: By induction on |remdups P | (where remdups removes duplicates), there must exist a derivation of the form wstate_of (N , P, O, t) * w2 wstate_of ([], P, O, t) w9 wstate_of (N ′ , P ′ , (C, i) # O, t + 1) * w wstate_of ([], [],

https://bitbucket.org/isafol/isafol/wiki/Home

https://bitbucket.org/isafol/isafol/src/master/Functional_Ordered_ Resolution_Prover/

http://matryoshka.gforge.inria.fr/pubs/fun_rp_data.tar.gz

Acknowledgments

Johannes Hölzl gave us some useful advice on how to specify and reason about possibly nonterminating functions in Isabelle/HOL. Alexander Bentkamp, Mathias Fleury, Andreas Halkjaer From, Carsten Fuhs, Peter Lammich, Mark Summerfield, Jørgen Villadsen, and the anonymous reviewers suggested many textual improvements. Eugene Kotelnikov, Stephan Schulz, and Geoff Sutcliffe graciously answered our questions about Vampire, E, and TPTP.

Schlichtkrull has received funding from a Ph.D. scholarship in the Algorithms, Logic and Graphs section of DTU Compute and from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 700321, LIGHTest). Blanchette has received funding from the ERC under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). An earlier version of this paper was included as a chapter of Schlichtkrull's Ph.D. thesis [36] with the same authors' list.


domain: math shs

text:
Sabine Schlager
email: sabine.schlager@uni-due.de

Jana Kaulvers
email: jana.kaulvers@uni-due.de

Andreas Büchter
email: andreas.buechter@uni-due.de

Effects of linguistic variations of word problems on the achievement in high stakes tests

Keywords: Language proficiency, difficulty level, item analysis, language obstacles, mathematics achievement

In Germany, as in other countries, language proficiency impacts the achievement in mathematics. Linguistic features may constitute possible obstacles for students solving word problems. This study explores the interplay of language proficiency and achievement in mathematics with tasks in which linguistic characteristics were varied experimentally. 640 10 th grade students solved the tasks. An analysis of the shift in difficulty of linguistically varied tasks indicates an irregular scheme: Only tasks with extreme variation of linguistic aspects, for example many nominalizations, show a significant shift. Data collected from student interviews using the think-aloud method show that linguistic aspects can be obstacles and therefore have an impact on the solution process, even if these linguistic aspects may not have an impact on the results in the quantitative part of the study.

unknown or polysemous words on a vocabulary level as linguistic features creating difficulties (Martiniello, 2008).

For the German language context, there are only a few studies about linguistic obstacles. For example, noun phrases and the number of academic language words seem to be difficult. The identified obstacles of word problems in the study by [START_REF] Prediger | Sprachkompetenz und Mathematikleistung-Empirische Untersuchung sprachlich bedingter Hürden in den Zentralen Prüfungen 10[END_REF] included prepositions, complex syntax and nominalizations. The obstacles did not only occur in the context of reading, but more often they were related to conceptual understanding. In this study the specific linguistic features which made the text complicated could not be isolated as they interacted with each other as well as with the mathematical content. With the experimental approach in our study, we strived to address this issue. For the specific context of the German language, we wanted to specify to what extent linguistic aspects could explain the achievement gap between students of higher and lower language proficiency by investigating the questions:

Q1. What impact do different linguistic aspects have on the achievement in literacy-based tests? Q2. Which linguistic aspects are difficult for (lower language proficient) students?

Research design and methods for the mixed-methods study

Context of the study

The mathematical tasks of the study were oriented towards the literacy-based high stakes exam "Zentrale Prüfungen am Ende der Klasse 10 (ZP10)" [central examinations at the end of 10 th grade] of North-Rhine-Westphalia (NRW), the most populous federal state of Germany. The ZP10-exam is designed by QUA-LiS NRW, the "Qualitätsund UnterstützungsAgentur -Landesinstitut für Schule NRW" [Quality and support agency -Institute for school NRW] that supports the Ministry of Education and lifelong learning in NRW. The exam does not only assess mathematical competencies acquired in 10 th grade, but also the competencies acquired during grade 5 to 10. For that reason, our tasks are required to illustrate different mathematical levels.

Design for the quantitative part of the study

The sample consists of 640 students from ten different comprehensive schools in the metropolitan area of Rhine-Ruhr. As independent variables, we collected information about students' language proficiency, cognitive capabilities and family background (cf. Table 1). Another important variable was the linguistic variation in the tasks. The dependent variable was mathematics achievement.

Language proficiency was measured using a standardized C-Test. Cognitive capabilities were measured by the extended standardized German adaption CFT-20R of culture fair intelligence tests. Information about family background (socio-economic status, immigrant status, languages spoken at home) was collected by questionnaire.

The mathematics test was designed referring to the ZP10-tests. Members of QUA-LiS NRW assured that our test would be acceptable for the high-stakes exam. The 90 minutes long test contained the typical topics of ZP10functions, descriptive statistics and percentage calculationwhich appear in the exam every year. These tasks were also chosen since the study of [START_REF] Prediger | Sprachkompetenz und Mathematikleistung-Empirische Untersuchung sprachlich bedingter Hürden in den Zentralen Prüfungen 10[END_REF] revealed many language obstacles in tasks about these topics. These observations are supported by results of Martiniello (2008) who identified data analysis, statistics and probability as topics that were difficult for English learners with Spanish as native language in the US.

The test was presented in three versions (A, B and C) with six identical anchor tasks (21 items) and six tasks with linguistic variation (13 items). The tasks with variation always existed in three different versions; the context and mathematical content remained unchanged at all times. In the initial version, we avoided difficult linguistic structures in the tasks, especially those structures that were varied in the other versions. Besides this initial version, the tasks were varied using two of the four linguistic features context vocabulary, verbs followed by prepositions or separable verbs, nominalization and density of the text, and reference structure, which were chosen out of possible linguistic obstacles in word problems reported in Prediger et al.'s study (2015).

On the word level, we chose the criterion "context vocabulary", which often causes problems butin contrast to technical termscan be changed without having influence on the mathematical content. Concerning the syntactical level, interviews in the study of [START_REF] Prediger | Sprachkompetenz und Mathematikleistung-Empirische Untersuchung sprachlich bedingter Hürden in den Zentralen Prüfungen 10[END_REF] confirmed the linguistic supposition that it is difficult for students to connect information given in sentences with separated separable verbs or between a verb and its preposition. Since Uesseler, Runge and Redder (2013) also state that separable verbs influence the understanding negatively, we selected these two features as a variation-category. As mathematical texts are often very dense and their length and density play an important role in student's understanding, the feature "density of the text" was chosen. This goes hand in hand with the feature "nominalization", because a dense text implies (in German) the use of many nominalizations which have a negative effect on the understanding [START_REF] Uesseler | Bildungssprache" diagnostizieren. Entwicklung eines Instruments zur Erfassung von bildungssprachlichen Fähigkeiten bei Viert-und Fünftklässlern[END_REF]. Therefore, these two features form one variation-category on the text-level. As mathematical texts try to avoid repetitions, the reference structure is often unclear. This led to consideration of "reference structure" as another category on the text-level. An example of a varied task will be presented later.

The groups of students sitting for the tests A, B or C were systematically formed based on the results from the C-Test and the CFT-20R. The variations were dispersed equally to the three versions of the test. There were no statistically significant differences between the groups concerning language proficiency, cognitive capabilities and mathematics achievement.

For data analysis, different statistical analysis procedures were applied. We split the group in half depending on students' results on the C-Test into groups of students with lower (C0) and higher (C1) language proficiency. The mathematical items were scaled using a Rasch model. An analysis of variance (univariate ANOVA) and a regression analysis were used to identify the background factors with the highest impact on mathematics achievement and to determine the explained variance. The shift in difficulty from the initial version of a word problem to its linguistic variation was determined by an analysis of the change of the WLE for these items on the Rasch scale.

Design for the qualitative part of the study

The purpose of this part of the study was to gain a deeper understanding of the quantitative results through a qualitative approach. For this reason, four tasks were presented to N=32 students with different levels of language proficiency from different comprehensive schools. The students were required to solve the designed tasks independently using the think-aloud method. Once the students solved the task, there was a discussion about the task between interviewer and student. All processes and discussions were videotaped, transcribed, and analyzed interpretatively with respect to whether the linguistic variations created difficulties for the students.

Examples of linguistic variation of tasks

An example of the linguistic variation of a particular task is represented in the translated initial version (1) and its variation "nominalization/dense structure" (2) of the task "Bathtub".

(1) A bathtub has one cold water tap and one hot water tap. The bathtub can be filled with 135 liters of water. If both water taps are open, it takes 9 minutes until the bathtub is filled completely. If only the cold water tap is open, it takes 7.5 minutes more than with both water taps open. How much water runs out of the opened cold water tap per minute? Note your calculations.

(2) A bathtub with one cold and one hot water tap can be filled with 135 liters of water. Opening both water taps, the filling of the bathtub takes 9 minutes; exclusively opening the cold water tap, it takes 7.5 minutes more than by opening both water taps. Which amount of water runs out of the opened cold water tap per minute? Note your calculations.

The bolded words or phrases show the variations in the task for this article. The translation of the tasks can only give an idea of the linguistic aspects that have been changed during variation, because most characteristics are inherent to the German language and sentence structure. For example, if you try to nominalize "the cold water tap is open [der Kaltwasserhahn ist geöffnet]" into "opening the cold water tap [Öffnung des Kaltwasserhahns]", in German, it implies the genitive case of "the cold water tap" tagged by an additive "s" at the end of the word ["Kaltwasserhahns"].

The variation of the items was not possible in every case, because of the structure of the German language. Sometimes it was impossible to use alternative formulations using the defined categories and employing them at positions in the text that are significant for the mathematical solution. The variations were limited due to the common use of language, the context and the linguistic realization of mathematical concepts. In addition, we had to accept the fact that variation of isolated linguistic aspects is almost impossible. In the German version of "If only the cold water tap is open [Wenn nur der Kaltwasserhahn geöffnet ist]", we find the participle II of the verb "open [geöffnet]" (in the English sentence it has the function as an adjective) because of the use of passive voice "is open [ist geöffnet]". This has to be nominalized. In the nominalized version, it is linguistically not possible to continue to use the familiar adverb "only [nur]" but necessary to use the less frequently used adjective "exclusively [ausschließlich]", which imposes another possible lexical obstacle.

Selected results

Impact of background factors

To check if linguistic features can explain the achievement gap due to different levels of language proficiency, we first analyzed the impact of background factors in our study. The results provide additional support for evidence of the impact of language proficiency on mathematics achievement. Students with higher intelligence or higher language proficiency, without immigrant status, and students who only speak German at home had statistically significant better results in the mathematics test (see Table 1, the number of the test persons varies because not all students gave the questioned information).

Regression analysis shows that language proficiency and cognitive capabilities as isolated background factors have the highest impact on mathematics achievement. They both explain about 15 % of the variance. The other background factors explain much less: Univariate variance analysis showed only low explanation potential of immigrant status (12 %), languages spoken at home (8 %) and socio-economic status (1 %). As language proficiency has such a high impact in our study, we investigated if it is possible to explain the achievement gap by the introduced linguistic obstacles.

Background factor Specification of groups

Distribution of groups

Mean score (WLE), m(SD)

Shifts in difficulty due to linguistic variation

All results for the different variations have been scaled in a Rasch model. Shifts in difficulty due to the linguistic variation were identified especially in Item 6 "Bathtub". In the initial version, 69 % of the C1-students and 48 % of the C0-students solved the item correctly. This shows that the initial version was easy for C1-students and common for C0-students. In the nominalized version with dense structure, half of the C1-students solved the item correctly compared to only 37 % of the C0students. The varied version was common for C1-students and difficult for C0-students.

Figure 1 depicts the shift in difficulty for the variations in comparison to the initial version. In comparison to the initial version, the denser text containing nominalizations became 0.6 WLE more difficult on the Rasch scale, comparable to three out of 34 correctly solved items in our study. Other items of this variation had no significant shift in difficulty (see Figure 1, left side). Students who only did tasks formulated like Item 2b would solve one item less correctly (0.2 WLE = 1 item); students who only had tasks formulated like Item 2a or 8a would solve the test basically the same. One explanation for the increasing difficulty of "Bathtub" is that this item is linguistically more difficult than others with the same linguistic variation, as the Flesch-Reading-Ease index shows.

The variation "reference structure" equally evoked a shift of 0.6 WLE for Item 6 "Bathtub". Other items with variation showed inconsistent shifts. Some items became more difficult, other items less difficult. A possible explanation is the higher relevance of mathematical content in contrast to language in particular items. For example, language has less effect in Item 8a, "What is the median?". In this case it is more important that the concept of median has been taught in mathematics classroom. Similar irregular shifts are visible for the other variations. In summary, linguistic variations make word problems more difficult, when applied often and when the general difficulty for understanding the word problem (cf. Flesch-index) increases greatly because of the application of these variations. In these cases, we talk about "extreme variations". Slight variations with only few modifications, which do not increase the difficulty for understanding, do not have statistically significant shifts. As the effect fluctuates substantially between different items, we can presume that the topic of a task is very important.

Linguistic variations as source for mathematical difficulty

The fact that the difficulty does not increase significantly for all items (with linguistic variation) does not imply that linguistic variation does not evoke obstacles for students, as our qualitative analysis highlights. Furthermore, we have observed that linguistic aspects do not create difficulty on their own, but in combination with other characteristics of the task as illustrated below.

In addition to the quantitative data, 16 tenth grade students solved the item "Bathtub" in the version "nominalization/dense structure" during the interviews. In particular, students with lower language proficiency had difficulties in understanding the word "exclusively [ausschließlich]", which had to be used due to the nominalization. While reading the text aloud, several students were puzzled by this word and explained they would never use it. This problem has already caused wrong solutions in the tests. One student wrote: "I do not understand the question. Does 'exclusively opening the cold water tap' mean that only the cold water tap is used?" He knew the correct meaning of "exclusively" but he was not sure about it. Probably, this was the reason he did not solve this item.

The nominalization "Opening [Öffnung]" of "to open [öffnen]" and the following genitive case of "the cold water tap [der Kaltwasserhahn]" also caused understanding problems, as the genitive case of "cold water tap [Kaltwasserhahn]" finishes with an 's' " [Kaltwasserhahns]" which in German is sometimes also a cue for plural of a word. In this case, the plural would be [Kaltwasserhähne].

Student:

I was confused by the word "Kaltwasserhahns". Does it mean two water taps or only one?

Apart from the linguistic variation, we identified other difficulties in our interviews. In particular, students with lower language proficiency had problems in understanding the relation "more than" and made wrong calculations. One student thinking aloud said (after three minutes of task solving):

Student: Ah, now I made a wrong calculation […] I thought that … the filling takes 7.5 minutes, but it takes 7.5 minutes MORE. I have to do a new calculation.

In the final discussion, many students could identify the relevant information "more than" and "exclusively opening the cold water tap" on their own or after a question from the interviewer. This shows that, even if there are difficulties in understanding the text, most of the students could solve the task if they had enough time and could verbalize their thoughts aloud. In contrast, in the tests, students often stopped solving a task because of uncertainty concerning their understanding.

Conclusion and consequences

Our outcome concerning Q1 is that linguistic variations had significant impact when the task varied in an extreme way. The fact that in German isolated variations have no overall significant impact evokes the hypothesis that they create difficulty in combination with each other or with other characteristics of the tasks. This hypothesis is supported by the qualitative results showing that not only the linguistic feature itself, such as nominalizations, but also the linguistic structures evoked by this feature, such as genitive cases, create difficulty. However, this has to be analyzed further.

In the context of Q2, in German, nominalization/dense structure, academic words such as "exclusively [ausschließlich]" or genitive cases are obstacles for several students, especially those of lower language proficiency. This was, for example, prominent in the results of lower language proficient students for the item "Bathtub". Students struggled in understanding these structures, which sometimes lead to not solving the task. When students had a lot of time and could speak out their thoughts, they reflected on these difficulties.

Consequences of this study for test construction are that high stakes tests should try to avoid extremely difficult linguistic structures, e.g. due to the frequent use of nominalizations, to reduce the achievement gap. Our study also showed that linguistic difficulties cannot always be avoided because there are constraints in the language. A consequence for mathematics classrooms that has emerged from students' ability to overcome linguistic difficulties by talking about them in our interviews, would be to explicitly address language issues and not to avoid linguistic difficulties.

The fact that our results pertaining to the effects of linguistic variations cannot explain the achievement gap, entails further and deeper research on the interplay between language proficiency and mathematics achievement in order to determine the nature of this correlation. A hypothesis that came up in our study and will be investigated is that the selection of strategies by students and their processes of solving tasks differ according to their language proficiency.

Figure 1 :

 1 Figure 1: Shift in difficulty compared to initial version (in WLE)

Table 1 : Distribution and differences among groups

 1

	Significant
	differences

Proceedings of CERME10

Acknowledgment

We would like to thank Claudia Benholz, who was part of the project team as a linguistic expert, Susanne Prediger for the discussion and advice, and QUA-LiS NRW for funding this study.