Peter Baumgartner
email: peter.baumgartner@data61.csiro.au

Uwe Waldmann

Hierarchic Superposition Revisited

Keywords: Automated deduction, Superposition calculus, Combinations of theories

published or not. The documents may come

Introduction

Many applications of automated deduction require reasoning with respect to a combination of a background theory, say integer arithmetic, and a foreground theory that extends the background theory by new sorts such as list, new operators, such as cons : int × list → list and length : list → int, and first-order axioms. Developing corresponding automated reasoning systems that are also able to deal with quantified formulas has recently been an active area of research. One major line of research is concerned with extending (SMT-based) solvers [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF] for the quantifier-free case by instantiation heuristics for quantifiers [17, 18, e. g.].

Another line of research is concerned with adding black-box reasoners for specific background theories to first-order automated reasoning methods (resolution [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF][START_REF] Korovin | Integrating linear arithmetic into superposition calculus[END_REF][START_REF] Althaus | Superposition modulo linear arithmetic SUP(LA)[END_REF], sequent calculi [START_REF] Rümmer | A constraint sequent calculus for first-order logic with linear integer arithmetic[END_REF], instantiation methods [START_REF] Ganzinger | Theory instantiation[END_REF][START_REF] Baumgartner | ME(LIA) -Model Evolution With Linear Integer Arithmetic Constraints[END_REF][START_REF] Baumgartner | Model evolution with equality modulo built-in theories[END_REF], etc). In both cases, a major unsolved research challenge is to provide reasoning support that is "reasonably complete" in practice, so that the systems can be used more reliably for both proving theorems and finding counterexamples.

In [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF], Bachmair, Ganzinger, and Waldmann introduced the hierarchical superposition calculus as a generalization of the superposition calculus for blackbox style theory reasoning. Their calculus works in a framework of hierarchic specifications. It tries to prove the unsatisfiability of a set of clauses with respect to interpretations that extend a background model such as the integers with linear arithmetic conservatively, that is, without identifying distinct elements of old sorts ("confusion") and without adding new elements to old sorts ("junk"). While confusion can be detected by first-order theorem proving techniques, junk can not -in fact, the set of logical consequences of a hierarchic specifications is usually not recursively enumerable. Refutational completeness can therefore only be guaranteed if one restricts oneself to sets of formulas where junk can be excluded a priori. The property introduced by Bachmair, Ganzinger, and Waldmann for this purpose is called "sufficient completeness with respect to simple instances". Given this property, their calculus is refutationally complete for clause sets that are fully abstracted (i. e., where no literal contains both foreground and background symbols). Unfortunately their full abstraction rule may destroy sufficient completeness with respect to simple instances. We show that this problem can be avoided by using a new form of clause abstraction and a suitably modified hierarchical superposition calculus. Since the new calculus is still refutationally complete and the new abstraction rule is guaranteed to preserve sufficient completeness with respect to simple instances, the new combination is strictly more powerful than the old one.

In practice, sufficient completeness is a rather restrictive property. While there are application areas where one knows in advance that every input is sufficiently complete, in most cases this does not hold. As a user of an automated theorem prover, one would like to see a best effort behavior: The prover might for instance try to make the input sufficiently complete by adding further theory axioms. In the calculus from [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF], this does not help at all: The restriction to a particular kind of instantiations ("simple instances") renders theory axioms essentially unusable in refutations. We show that this can be prevented by introducing two kinds of variables of the background theory sorts, that can be instantiated in different ways, making our calculus significantly "more complete" in practice. We also include a definition rule in the calculus that can be used to establish sufficient completeness by linking foreground terms to background parameters, thus allowing the background prover to reason about these terms.

The following trivial example demonstrates the problem. Consider the clause set N = {C} where C = f(1) < f [START_REF] Althaus | Superposition modulo linear arithmetic SUP(LA)[END_REF]. Assume that the background theory is integer arithmetic and that f is an integer-sorted operator from the foreground (free) signature. Intuitively, one would expect N to be unsatisfiable. However, N is not sufficiently complete, and it admits models in which f(1) is interpreted as some junk element / c, an element of the domain of the integer sort that is not a numeric constant. So both the calculus in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] and ours are excused to not find a refutation. To fix that, one could add an instance C = ¬(f(1) < f(1)) of the irreflexivity axiom ¬(x < x). The resulting set N = {C, C } is (trivially) sufficiently complete as it has no models at all. However, the calculus in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] is not helped by adding C , since the abstracted version of N is again not sufficiently complete and admits a model that interprets f(1) as / c. Our abstraction mechanism always preserves sufficient completeness and our calculus will find a refutation.

With this example one could think that replacing the abstraction mechanism in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] with ours gives all the advantages of our calculus. But this is not the case. Let N = {C, ¬(x < x)} be obtained by adding the more realistic axiom ¬(x < x). The set N is still sufficiently complete with our approach thanks to having two kinds of variables at disposal, but it is not sufficiently complete in the sense of [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF]. Indeed, in that calculus adding background theory axioms never helps to gain sufficient completeness, as variables there have only one kind.

Another alternative to make N sufficiently complete is by adding a clause that forces f(1) to be equal to some background domain element. For instance, one can add a "definition" for f [START_REF] Althaus | Superposition modulo linear arithmetic SUP(LA)[END_REF], that is, a clause f(1) ≈ α, where α is a fresh symbolic constant belonging to the background signature (a "parameter"). The set N = {C, f(1) ≈ α} is sufficiently complete and it admits refutations with both calculi. The definition rule in our calculus mentioned above will generate this definition automatically. Moreover, the set N belongs to a syntactic fragment for which we can guarantee not only sufficient completeness (by means of the definition rule) but also refutational completeness.

We present the new calculus in detail and provide a general completeness result, modulo compactness of the background theory, and two specific completeness results for clause sets that do not require compactness -one for the fragment where all background-sorted terms are ground and another one for a special case of linear (integer or rational) arithmetic as a background theory.

We also report on experiments with a prototypical implementation on the TPTP problem library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0[END_REF].

Sections 1-7, 9-10, and 12 of this paper are a substantially expanded and revised version of [START_REF] Baumgartner | Hierarchic superposition with weak abstraction[END_REF]. A preliminary version of Sect. 11 has appeared in [START_REF] Baumgartner | Hierarchic superposition: Completeness without compactness[END_REF].However, we omit from this paper some proofs that are not essential for the understanding of the main ideas. They can be found in a slightly extended version of this paper at http://arxiv.org/abs/1904.03776 [START_REF] Baumgartner | Hierarchic superposition revisited[END_REF].

Related Work. The relation with the predecessor calculus in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] is discussed above and also further below. What we say there also applies to other developments rooted in that calculus, [1, e. g.]. The specialized version of hierarchic superposition in [START_REF] Kruglov | Superposition decides the first-order logic fragment over ground theories[END_REF] will be discussed in Sect. 9 below. The resolution calculus in [START_REF] Korovin | Integrating linear arithmetic into superposition calculus[END_REF] has built-in inference rules for linear (rational) arithmetic, but is complete only under restrictions that effectively prevent quantification over rationals. Earlier work on integrating theory reasoning into model evolution [START_REF] Baumgartner | ME(LIA) -Model Evolution With Linear Integer Arithmetic Constraints[END_REF][START_REF] Baumgartner | Model evolution with equality modulo built-in theories[END_REF] lacks the treatment of background-sorted foreground function symbols. The same applies to the sequent calculus in [START_REF] Rümmer | A constraint sequent calculus for first-order logic with linear integer arithmetic[END_REF], which treats linear arithmetic with built-in rules for quantifier elimination. The instantiation method in [START_REF] Ganzinger | Theory instantiation[END_REF] requires an answercomplete solver for the background theory to enumerate concrete solutions of background constraints, not just a decision procedure. All these approaches have in common that they integrate specialized reasoning for background theories into a general first-order reasoning method. A conceptually different approach consists in using first-order theorem provers as (semi-)decision procedures for specific theories in DPLL(T)(-like) architectures [START_REF] De Moura | Engineering DPLL(T) + saturation[END_REF][START_REF] Armando | New results on rewritebased satisfiability procedures[END_REF][START_REF] Bonacina | On deciding satisfiability by theorem proving with speculative inferences[END_REF]. Notice that in this context the theorem provers do not need to reason modulo background theories themselves, and indeed they don't. The calculus and system in [START_REF] De Moura | Engineering DPLL(T) + saturation[END_REF], for instance, integrates superposition and DPLL(T). From DPLL(T) it inherits splitting of ground non-unit clauses into their unit components, which determines a (backtrackable) model candidate M . The superposition inference rules are applied to elements from M and a current clause set F . The superposition component guarantees refutational completeness for pure first-order clause logic. Beyond that, for clauses containing background-sorted variables, (heuristic) instantiation is needed. Instantiation is done with ground terms that are provably equal w. r. t. the equations in M to some ground term in M in order to advance the derivation. The limits of that method can be illustrated with an (artificial but simple) example. Consider the unsatisfiable clause set {i ≤ j ∨ P(i + 1, x) ∨ P(j + 2, x), i ≤ j ∨ ¬P(i + 3, x) ∨ ¬P(j + 4, x)} where i and j are integer-sorted variables and x is a foreground-sorted variable. Neither splitting into unit clauses, superposition calculus rules, nor instantiation applies, and so the derivation gets stuck with an inconclusive result. By contrast, the clause set belongs to a fragment that entails sufficient completeness ("no background-sorted foreground function symbols") and hence is refutable by our calculus. On the other hand, heuristic instantiation does have a place in our calculus, but we leave that for future work.

Signatures, Clauses, and Interpretations

We work in the context of standard many-sorted logic with first-order signatures comprised of sorts and operator (or function) symbols of given arities over these sorts. A signature is a pair Σ = (Ξ, Ω), where Ξ is a set of sorts and Ω is a set of operator symbols over Ξ. If X is a set of sorted variables with sorts in Ξ, then the set of well-sorted terms over Σ = (Ξ, Ω) and X is denoted by T Σ (X ); T Σ is short for T Σ (∅). We require that Σ is a sensible signature, i. e., that T Σ has no empty sorts. As usual, we write t[u] to indicate that the term u is a (not necessarily proper) subterm of the term t. The position of u in t is left implicit.

A Σ-equation is an unordered pair (s, t), usually written s ≈ t, where s and t are terms from T Σ (X ) of the same sort. For simplicity, we use equality as the only predicate in our language. Other predicates can always be encoded as a function into a set with one distinguished element, so that a non-equational atom is turned into an equation P (t 1 , . . . , t n ) ≈ true P ; this is usually abbreviated by P (t 1 , . . . , t n ). 3 A literal is an equation s ≈ t or a negated equation ¬(s ≈ t), also written as s ≈ t. A clause is a multiset of literals, usually written as a disjunction; the empty clause, denoted by is a contradiction. If F is a term, equation, literal or clause, we denote by vars(F ) the set of variables that occur in F . We say F is ground if vars(F ) = ∅ A substitution σ is a mapping from variables to terms that is sort respecting, that is, maps each variable x ∈ X to a term of the same sort. Substitutions are homomorphically extended to terms as usual. We write substitution application in postfix form. A term s is an instance of a term t if there is a substitution σ such that tσ = s. All these notions carry over to equations, literals and clauses in the obvious way. The composition στ of the substitutions σ and τ is the substitution that maps every variable x to (xσ)τ .

The domain of a substitution σ is the set dom(σ) = {x | x = xσ}. We use only substitutions with finite domains, written as

σ = [x 1 → t 1 , . . . , x n → t n ]
where dom(σ) = {x 1 , . . . , x n }. A ground substitution is a substitution that maps every variable in its domain to a ground term. A ground instance of F is obtained by applying some ground substitution with domain (at least) vars(F ) to it.

A Σ-interpretation I consists of a Ξ-sorted family of carrier sets {I ξ } ξ∈Ξ and of a function

I f : I ξ1 × • • • × I ξn → I ξ0 for every f : ξ 1 . . . ξ n → ξ 0 in Ω. The interpretation t I of a ground term t is defined recursively by f (t 1 , . . . , t n ) I = I f (t I 1 , . . . , t I n ) for n ≥ 0.
An interpretation I is called term-generated, if every element of an I ξ is the interpretation of some ground term of sort ξ. An interpretation I is said to satisfy a ground equation s ≈ t, if s and t have the same interpretation in I; it is said to satisfy a negated ground equation s ≈ t, if s and t do not have the same interpretation in I. The interpretation I satisfies a ground clause C if at least one of the literals of C is satisfied by I. We also say that a ground clause C is true in I, if I satisfies C; and that C is false in I, otherwise. A term-generated interpretation I is said to satisfy a non-ground clause C if it satisfies all ground instances Cσ; it is called a model of a set N of clauses, if it satisfies all clauses of N . 4 We abbreviate the fact that I If J is a class of Σ-interpretations, a Σ-clause or clause set is called Jsatisfiable if at least one I ∈ J satisfies the clause or clause set; otherwise it is called J -unsatisfiable.

A specification is a pair SP = (Σ, J ), where Σ is a signature and J is a class of term-generated Σ-interpretations called models of the specification SP . We assume that J is closed under isomorphisms.

We say that a class of Σ-interpretations J or a specification (Σ, J ) is compact, if every infinite set of Σ-clauses that is J -unsatisfiable has a finite subset that is also J -unsatisfiable.

Hierarchic Theorem Proving

In hierarchic theorem proving, we consider a scenario in which a general-purpose foreground theorem prover and a specialized background prover cooperate to de-rive a contradiction from a set of clauses. In the sequel, we will usually abbreviate "foreground" and "background" by "FG" and "BG".

The BG prover accepts as input sets of clauses over a BG signature Σ B = (Ξ B , Ω B ). Elements of Ξ B and Ω B are called BG sorts and BG operators, respectively. We fix an infinite set X B of BG variables of sorts in Ξ B . Every BG variable has (is labeled with) a kind, which is either "abstraction" or "ordinary". Terms over Σ B and X B are called BG terms. A BG term is called pure, if it does not contain ordinary variables; otherwise it is impure. These notions apply analogously to equations, literals, clauses, and clause sets.

The BG prover decides the satisfiability of Σ B -clause sets with respect to a BG specification (Σ B , B), where B is a class of term-generated Σ B -interpretations called BG models. We assume that B is closed under isomorphisms.

In most applications of hierarchic theorem proving, the set of BG operators

Ω B contains a set of distinguished constant symbols Ω D B ⊆ Ω B that has the property that d I 1 = d I 2 for any two distinct d 1 , d 2 ∈ Ω D
B and every BG model I ∈ B. We refer to these constant symbols as (BG) domain elements.

While we permit arbitrary classes of BG models, in practice the following three cases are most relevant:

(1) B consists of exactly one Σ B -interpretation (up to isomorphism), say, the integer numbers over a signature containing all integer constants as domain elements and ≤, <, +, -with the expected arities. interpretations that satisfy some first-order theory, say, the first-order theory of linear integer arithmetic. 5 Since B corresponds to a first-order theory, compactness is recovered. It should be noted, however, that B contains nonstandard models, so that for instance the clause set

{ n ≤ β | n ∈ N } is now satisfiable (e. g., Q × Z with a lexicographic ordering is a model).
The FG theorem prover accepts as inputs clauses over a signature Σ = (Ξ, Ω), where Ξ B ⊆ Ξ and Ω B ⊆ Ω. The sorts in Ξ F = Ξ \ Ξ B and the operator symbols in Ω F = Ω \ Ω B are called FG sorts and FG operators. Again we fix an infinite set X F of FG variables of sorts in Ξ F . All FG variables have the kind "ordinary". We define X = X B ∪ X F .

In examples we will use {0, 1, 2, . . . } to denote BG domain elements, {+, -, <, ≤} to denote (non-parameter) BG operators, and the possibly subscripted letters {x, y}, {X, Y }, {α, β}, and {a, b, c, f, g} to denote ordinary variables, abstraction variables, parameters, and FG operators, respectively. The letter ζ denotes an ordinary variable or an abstraction variable.

We call a term in T Σ (X ) a FG term, if it is not a BG term, that is, if it contains at least one FG operator or FG variable (and analogously for literals or clauses). We emphasize that for a FG operator f : ξ 1 . . . ξ n → ξ 0 in Ω F any of the ξ i may be a BG sort, and that consequently FG terms may have BG sorts.

If I is a Σ-interpretation, the restriction of I to Σ B , written I| ΣB , is the Σ Binterpretation that is obtained from I by removing all carrier sets I ξ for ξ ∈ Ξ F and all functions I f for f ∈ Ω F . Note that I| ΣB is not necessarily term-generated even if I is term-generated. In hierarchic theorem proving, we are only interested in Σ-interpretations that extend some model in B and neither collapse any of its sorts nor add new elements to them, that is, in Σ-interpretations I for which I| ΣB ∈ B. We call such a Σ-interpretation a B-interpretation.

Let N and N be two sets of Σ-clauses. We say that N entails N relative to B (and write

N |= B N ), if every model of N whose restriction to Σ B is in B is a model of N . Note that N |= B N follows from N |= N . If N |= B ,
we call N B-unsatisfiable; otherwise, we call it B-satisfiable. 6Our goal in refutational hierarchic theorem proving is to check whether a given set of Σ-clauses N is false in all B-interpretations, or equivalently, whether N is B-unsatisfiable.

We say that a substitution σ is simple if Xσ is a pure BG term for every abstraction variable X ∈ dom(σ). For example, [x → 1+Y +α], [X → 1+Y +α] and [x → f(1)] all are simple, whereas [X → 1 + y + α] and [X → f(1)] are not. Let F be a clause or (possibly infinite) clause set. By sgi(F ) we denote the set of simple ground instances of F , that is, the set of all ground instances of (all clauses in) F obtained by simple ground substitutions.

For a BG specification (Σ B , B), we define GndTh(B) as the set of all ground Σ B -formulas that are satisfied by every I ∈ B. Definition 3.1 (Sufficient completeness). A Σ-clause set N is called sufficiently complete w. r. t. simple instances if for every Σ-model J of sgi(N ) ∪ GndTh(B) 7 and every ground BG-sorted FG term s there is a ground BG term t such that J |= s ≈ t. 8For brevity, we will from now on omit the phrase "w. r. t. simple instances" and speak only of "sufficient completeness". It should be noted, though, that our definition differs from the classical definition of sufficient completeness in the literature on algebraic specifications.

Orderings

A hierarchic reduction ordering is a strict, well-founded ordering on terms that is compatible with contexts, i. e., s t implies u[s] u[t], and stable under simple substitutions, i. e., s t implies sσ tσ for every simple σ. In the rest of this paper we assume such a hierarchic reduction ordering that satisfies all of the following: (i) is total on ground terms, (ii) s d for every domain element d and every ground term s that is not a domain element, and (iii) s t for every ground FG term s and every ground BG term t. These conditions are easily satisfied by an LPO with an operator precedence in which FG operators are larger than BG operators and domain elements are minimal with, for example, • • • -2 2 -1 1 0 to achieve well-foundedness.

Condition (iii) and stability under simple substitutions together justify to always order s X where s is a non-variable FG term and X is an abstraction variable. By contrast, s

x can only hold if x ∈ vars(s). Intuitively, the combination of hierarchic reduction orderings and abstraction variables affords ordering more terms.

The ordering is extended to literals over terms by identifying a positive literal s ≈ t with the multiset {s, t}, a negative literal s ≈ t with {s, s, t, t}, and using the multiset extension of . Clauses are compared by the multiset extension of , also denoted by .

The non-strict orderings are defined as s t if and only if s t or s = t (the latter is multiset equality in case of literals and clauses). A literal L is maximal (strictly maximal ) in a clause L ∨ C if there is no K ∈ C with K L (K L).

Weak Abstraction

To refute an input set of Σ-clauses, hierarchic superposition calculi derive BG clauses from them and pass the latter to a BG prover. In order to do this, some separation of the FG and BG vocabulary in a clause is necessary. The technique used for this separation is known as abstraction: One (repeatedly) replaces some term q in a clause by a new variable and adds a disequations to the clause, so that

C[q] is converted into the equivalent clause ζ ≈ q ∨ C[ζ],
where ζ is a new (abstraction or ordinary) variable.

The calculus by Bachmair, Ganzinger, and Waldmann [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] works on "fully abstracted" clauses: Background terms occurring below a FG operator or in an equation between a BG and a FG term or vice versa are abstracted out until one arrives at a clause in which no literal contains both FG and BG operators.

A problematic aspect of any kind of abstraction is that it tends to increase the number of incomparable terms in a clause, which leads to an undesirable growth of the search space of a theorem prover. For instance, if we abstract out the subterms t and t in a ground clause f(t) ≈ g(t ), we get x ≈ t ∨ y ≈ t ∨ f(x) ≈ g(y), and the two new terms f(x) and g(y) are incomparable in any reduction ordering. In [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] this problem is mitigated by considering only instances where BG-sorted variables are mapped to BG terms: In the terminology of the current paper, all BG-sorted variables in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] have the kind "abstraction". This means that, in the example above, we obtain the two terms f(X) and g(Y ). If we use an LPO with a precedence in which f is larger than g and g is larger than every BG operator, then for every simple ground substitution τ , f(X)τ is strictly larger that g(Y )τ , so we can still consider f(X) as the only maximal term in the literal.

The advantage of full abstraction is that this clause structure is preserved by all inference rules. There is a serious drawback, however: Consider the clause set N = { 1 + c ≈ 1 + c }. Since N is ground, we have sgi(N ) = N , and since sgi(N ) is unsatisfiable, N is trivially sufficiently complete. Full abstraction turns

N into N = { X ≈ c ∨ 1 + X ≈ 1 + X }.
In the simple ground instances of N , X is mapped to all pure BG terms. However, there are Σ-interpretations of sgi(N ) in which c is interpreted differently from any pure BG term, so sgi(N ) ∪ GndTh(B) does have a Σ-model and N is no longer sufficiently complete. In other words, the calculus of [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] is refutationally complete for clause sets that are fully abstracted and sufficiently complete, but full abstraction may destroy sufficient completeness. (In fact, the calculus is not able to refute N .)

The problem that we have seen is caused by the fact that full abstraction replaces FG terms by abstraction variables, which may not be mapped to FG terms later on. The obvious fix would be to use ordinary variables instead of abstraction variables whenever the term to be abstracted out is not a pure BG term, but as we have seen above, this would increase the number of incomparable terms and it would therefore be detrimental to the performance of the prover.

Full abstraction is a property that is stronger than actually necessary for the completeness proof of [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF]. In fact, it was claimed in a footnote in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] that the calculus could be optimized by abstracting out only non-variable BG terms that occur below a FG operator. This is incorrect, however: Using this abstraction rule, neither our calculus nor the calculus of [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] would be able to refute { 1+1 ≈ 2, (1 + 1) + c ≈ 2 + c }, even though this set is unsatisfiable and trivially sufficiently complete. We need a slightly different abstraction rule to avoid this problem: Definition 5.1. A BG term q is a target term in a clause C if q is neither a domain element nor a variable and if C has the form C[f (s 1 , . . . , q, . . . , s n )], where f is a FG operator or at least one of the s i is a FG or impure BG term. 9 A clause is called weakly abstracted if it does not have any target terms.

The weakly abstracted version of a clause is the clause that is obtained by exhaustively replacing C[q] by 9 Target terms are terms that need to be abstracted out; so for efficiency reasons, it is advantageous to keep the number of target terms as small as possible. We will show in Sect. 7 why domain elements may be treated differently from other non-variable terms. On the other hand, all the results in the following sections continue to hold if the restriction that q is not a domain element is dropped (i. e., if domain elements are abstracted out as well). We will make use of this fact in Sect. 11.

-C[X] ∨ X ≈ q, where X is a new abstraction variable, if q is a pure target term in C, -C[y] ∨ y ≈ q, where y is a new ordinary variable, if q is an impure target term in C.

The weakly abstracted version of a clause C is denoted by abstr(C); if N is a set of clauses then abstr(N ) = { abstr(C) | C ∈ N }.

For example, weak abstraction of the clause g(1, α, f(1) Nested abstraction is only necessary for certain impure BG terms. For instance, the clause f(z + α) ≈ 1 has two target terms, namely α (since z is an impure BG term) and z + α (since f is a FG operator). If we abstract out α, we obtain f(z + X) ≈ 1 ∨ X ≈ α. The new term z + X is still a target term, so one more abstraction step yields f(y) ≈ 1 ∨ X ≈ α ∨ y ≈ z + X. (Alternatively, we can first abstract out z + α, yielding f(y) ≈ 1 ∨ y ≈ z + α, and then α. The final result is the same.)

+ (α + 1), z) ≈ β yields g(1, X, f(1)+Y, z) ≈ β ∨X ≈ α∨Y ≈ α+1. Note that
It is easy to see that the abstraction process described in Def. 5.1 terminates by comparing the multisets of the numbers of non-variable occurrences in the left and right-hand sides of all literals before and after an abstraction step. Proposition 5.2. If N is a set of clauses and N is obtained from N by replacing one or more clauses by their weakly abstracted versions, then sgi(N ) and sgi(N ) are equivalent and N is sufficiently complete whenever N is.

Proof. Let us first consider the case of a single abstraction step applied to a single clause. Let C[q] be a clause with a target term q and let D = C[ζ] ∨ ζ ≈ q be the result of abstracting out q (where ζ is a new abstraction variable, if q is pure, and a new ordinary variable, if q is impure). We will show that sgi(C) and sgi(D) have the same models.

In one direction let I be an arbitrary model of sgi(C). We have to show that I is also a model of every simple ground instance Dτ of D. If I satisfies the disequation ζτ ≈ qτ then this is trivial. Otherwise, ζτ and qτ have the same interpretation in

I. Since dom(τ ) ⊇ vars(D) = vars(C) ∪ {ζ}, Cτ is a simple ground instance of C, so I is a model of Cτ = Cτ [qτ ]. By congruence, we conclude that I is also a model of Cτ [ζτ ], hence it is a model of Dτ = Cτ [ζτ ] ∨ ζτ ≈ qτ .
In the other direction let I be an arbitrary model of sgi(D). We have to show that I is also a model of every simple ground instance Cτ of C. Without loss of generality assume that ζ / ∈ dom(τ ). If ζ is an abstraction variable, then q is a pure BG term, and since τ is a simple substitution, qτ is a pure BG term as well. Consequently, the substitutions By induction over the number of abstraction steps we conclude that for any clause C, sgi(C) and sgi(abstr(C)) are equivalent. The extension to clause sets N and N follows then from the fact that I is a model of sgi(N ) if and only if it is a model of sgi(C) for all C ∈ N . Moreover, the equivalence of sgi(N ) and sgi(N ) implies obviously that N is sufficiently complete whenever N is.

In contrast to full abstraction, the weak abstraction rule does not require abstraction of FG terms (which can destroy sufficient completeness if done using abstraction variables, and which is detrimental to the performance of a prover if done using ordinary variables). BG terms are usually abstracted out using abstraction variables. The exception are BG terms that are impure, i. e., that contain ordinary variables themselves. In this case, we cannot avoid to use ordinary variables for abstraction, otherwise, we might again destroy sufficient completeness. For example, the clause set { P(1 + y), ¬P(1 + c) } is sufficiently complete. If we used an abstraction variable instead of an ordinary variable to abstract out the impure subterm 1 + y, we would get { P(X) ∨ X ≈ 1 + y, ¬P(1 + c) }, which is no longer sufficiently complete.

In input clauses (that is, before abstraction), BG-sorted variables may be declared as "ordinary" or "abstraction". As we have seen above, using abstraction variables can reduce the search space; on the other hand, abstraction variables may be detrimental to sufficient completeness. Consider the following example:

The set of clauses N = { ¬f(x) > g(x) ∨ h(x) ≈ 1, ¬f(x) ≤ g(x) ∨ h(x) ≈ 2, ¬h(x) > 0 }
is unsatisfiable w. r. t. linear integer arithmetic, but since it is not sufficiently complete, the hierarchic superposition calculus does not detect the unsatisfiability. Adding the clause X > Y ∨ X ≤ Y to N does not help: Since the abstraction variables X and Y may not be mapped to the FG terms f(x) and g(x) in a simple ground instance, the resulting set is still not sufficiently complete. However, if we add the clause x > y ∨ x ≤ y, the set of clauses becomes (vacuously) sufficiently complete and its unsatisfiability is detected.

One might wonder whether it is also possible to gain anything if the abstraction process is performed using ordinary variables instead of abstraction variables. The following proposition shows that this is not the case: Proposition 5.3. Let N be a set of clauses, let N be the result of weak abstraction of N as defined above, and let N be the result of weak abstraction of N where all newly introduced variables are ordinary variables. Then sgi(N ) and sgi(N ) are equivalent and sgi(N ) is sufficiently complete if and only if sgi(N ) is.

Proof. By Prop. 5.2, we know already that sgi(N ) and sgi(N ) are equivalent. Moreover, it is easy to check the proof of Prop. 5.2 is still valid if we assume that the newly introduced variable ζ is always an ordinary variable. (Note that the proof requires that abstraction variables are mapped only to pure BG terms, but it does not require that a variable that is mapped to a pure BG term must be an abstraction variable.) So we can conclude in the same way that sgi(N ) and sgi(N ) are equivalent, and hence, that sgi(N ) and sgi(N ) are equivalent. From this, we can conclude that N is sufficiently complete whenever N is.

Base Inference System

An inference system I is a set of inference rules. By an I inference we mean an instance of an inference rule from I such that all conditions are satisfied.

The base inference system HSP Base of the hierarchic superposition calculus consists of the inference rules Equality resolution, Negative superposition, Positive superposition, Equality factoring, and Close defined below. The calculus is parameterized by a hierarchic reduction ordering and by a "selection function" that assigns to every clause a (possibly empty) subset of its negative FG literals. All inference rules are applicable only to weakly abstracted premise clauses.

Equality resolution

s ≈ t ∨ C abstr(Cσ)
if (i) σ is a simple mgu of s and t, (ii) sσ is not a pure BG term, and (iii) if the premise has selected literals, then s ≈ t is selected in the premise, otherwise (s ≈ t)σ is maximal in (s ≈ t ∨ C)σ. 10For example, Equality resolution is applicable to

1 + c ≈ 1 + x with the simple mgu [x → c], but it is not applicable to 1+α ≈ 1+x, since 1+α is a pure BG term. Negative superposition l ≈ r ∨ C s[u] ≈ t ∨ D abstr((s[r] ≈ t ∨ C ∨ D)σ)
if (i) u is not a variable, (ii) σ is a simple mgu of l and u, (iii) lσ is not a pure BG term, (iv) rσ lσ, (v) (l ≈ r)σ is strictly maximal in (l ≈ r ∨ C)σ, (vi) the first premise does not have selected literals, (vii) tσ sσ, and (viii) if the second premise has selected literals, then s ≈ t is selected in the second premise, otherwise

(s ≈ t)σ is maximal in (s ≈ t ∨ D)σ. Positive superposition l ≈ r ∨ C s[u] ≈ t ∨ D abstr((s[r] ≈ t ∨ C ∨ D)σ) if (i) u is not a variable, (ii) σ is a simple mgu of l and u, (iii) lσ is not a pure BG term, (iv) rσ lσ, (v) (l ≈ r)σ is strictly maximal in (l ≈ r ∨ C)σ, (vi) tσ sσ, (vii) (s ≈ t)σ is strictly maximal in (s ≈ t ∨ D)σ,
and (viii) none of the premises has selected literals.

Equality factoring

s ≈ t ∨ l ≈ r ∨ C abstr((l ≈ r ∨ t ≈ r ∨ C)σ)
where (i) σ is a simple mgu of s and l, (ii) sσ is not a pure BG term, (iii) (s ≈ t)σ is maximal in (s ≈ t∨l ≈ r ∨C)σ, (iv) tσ sσ, (v) lσ rσ, and (vi) the premise does not have selected literals.

Close C 1 • • • C n if C 1 , . . . , C n are BG clauses and {C 1 , . . . , C n } is B-unsatisfiable, i. e., no inter- pretation in B is a Σ B -model of {C 1 , . . . , C n }.
Notice that Close is not restricted to take pure BG clauses only. The reason is that also impure BG clauses admit simple ground instances that are pure. All inference rules of HSP Base involve (simple) mgus. Because of the two kinds of variables, abstraction and ordinary ones, the practical question arises if standard unification algorithms can be used without or only little modification. For example, the terms Z and

(x + y) admit a simple mgu σ = [x → X, y → Y, Z → X + Y ].
This prompts for the use of weakening substitutions as in many-sorted logics with subsorts [START_REF] Walther | Many-sorted unification[END_REF].A closer inspection of the inference rules shows, however, that such substitutions never need to be considered: All unifiers computed in the inference rules have the property that abstraction variables are only mapped to abstraction variables or domain elements; apart from this additional restriction, we can use a standard unification algorithm.

In contrast to [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF], the inference rules above include an explicit weak abstraction in their conclusion. Without it, conclusions would not be weakly abstracted in general. For example Positive superposition applied to the weakly abstracted clauses f(X) ≈ 1 ∨ X ≈ α and P(f(1) + 1) would then yield P(1 + 1) ∨ 1 ≈ α, whose P-literal is not weakly abstracted. Additionally, the side conditions of our rules differ somewhat from the corresponding rules of [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF], this is due on the one hand to the presence of impure BG terms (which must sometimes be treated like FG terms), and on the other hand to the fact that, after weak abstraction, literals may still contain both FG and BG operators.

The inference rules are supplemented by a redundancy criterion, that is, a mapping R Cl from sets of formulae to sets of formulae and a mapping R Inf from sets of formulae to sets of inferences that are meant to specify formulae that may be removed from N and inferences that need not be computed. (R Cl (N ) need not be a subset of N and R Inf (N ) will usually also contain inferences whose premises are not in N .) Definition 6.2. A pair R = (R Inf , R Cl ) is called a redundancy criterion ( with respect to an inference system I and a consequence relation |=), if the following conditions are satisfied for all sets of formulae N and N :

(i) N \ R Cl (N ) |= R Cl (N ). (ii) If N ⊆ N , then R Cl (N ) ⊆ R Cl (N ) and R Inf (N ) ⊆ R Inf (N ). (iii) If ι is an inference and its conclusion is in N , then ι ∈ R Inf (N ). (iv) If N ⊆ R Cl (N ), then R Cl (N ) ⊆ R Cl (N \N ) and R Inf (N ) ⊆ R Inf (N \N ).
The inferences in R Inf (N ) and the formulae in R Cl (N ) are said to be redundant with respect to N .

Let SSP be the ground standard superposition calculus using the inference rules equality resolution, negative superposition, positive superposition, and equality factoring (Bachmair and Ganzinger [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF], Nieuwenhuis [START_REF] Nieuwenhuis | First-order completion techniques[END_REF], Nieuwenhuis and Rubio [START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF]). To define a redundancy criterion for HSP Base and to prove the refutational completeness of the calculus, we use the same approach as in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] and relate HSP Base inferences to the corresponding SSP inferences.

For a set of ground clauses N , we define R S Cl (N ) to be the set of all clauses C such that there exist clauses C 1 , . . . , C n ∈ N that are smaller than C with respect to and C 1 , . . . , C n |= C. We define R S Inf (N ) to be the set of all ground SSP inferences ι such that either a premise of ι is in R S Cl (N ) or else C 0 is the conclusion of ι and there exist clauses C 1 , . . . , C n ∈ N that are smaller with respect to c than the maximal premise of ι and C 1 , . . . , C n |= C 0 .

The following results can be found in [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF] and [START_REF] Nieuwenhuis | First-order completion techniques[END_REF]:

Theorem 6.3. The (ground) standard superposition calculus SSP and R S = (R S Inf , R S Cl ) satisfy the following properties: (i) R S is a redundancy criterion with respect to |=. (ii) SSP together with R S is refutationally complete.

Let ι be an HSP Base inference with premises C 1 , . . . , C n and conclusion abstr(C), where the clauses C 1 , . . . , C n have no variables in common. Let ι be a ground SSP inference with premises C 1 , . . . , C n and conclusion C . If σ is a simple substitution such that C = Cσ and C i = C i σ for all i, and if none of the C i is a BG clause, then ι is called a simple ground instance of ι. The set of all simple ground instances of an inference ι is denoted by sgi(ι). Definition 6.4. Let N be a set of weakly abstracted clauses. We define R H Inf (N ) to be the set of all inferences ι such that either ι is not a Close inference and sgi(ι) ⊆ R S Inf (sgi(N ) ∪ GndTh(B)), or else ι is a Close inference and ∈ N . We define R H Cl (N ) to be the set of all weakly abstracted clauses C such that sgi

(C) ⊆ R S Cl (sgi(N ) ∪ GndTh(B)) ∪ GndTh(B). 11

Refutational Completeness

To prove that HSP Base and R H = (R H Inf , R H Cl ) are refutationally complete for sets of weakly abstracted Σ-clauses and compact BG specifications (Σ B , B), we use the same technique as in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF]:

First we show that R H is a redundancy criterion with respect to |= B , and that a set of clauses remains sufficiently complete if new clauses are added or if redundant clauses are deleted.The proofs are rather technical and can be found in [START_REF] Baumgartner | Hierarchic superposition revisited[END_REF]. They are similar to the corresponding ones in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF]; the differences are due, on the one hand, to the fact that we include GndTh(B) in the redundancy criterion and in the definition of sufficient completeness, and, on the other hand, to the explicit abstraction steps in our inference rules.

Lemma 7.1. If sgi(N ) ∪ GndTh(B) |= sgi(C), then N |= B C. Proof. Suppose that sgi(N ) ∪ GndTh(B) |= sgi(C). Let I be a Σ-model of N whose restriction to Σ B is contained in B.
Clearly, I is also a model of GndTh(B). Since I does not add new elements to the sorts of I = I | ΣB and I is a termgenerated Σ B -interpretation, we know that for every ground Σ-term t of a BG sort there is a ground BG term t such that t and t have the same interpretation in I . Therefore, for every ground substitution σ there is an equivalent simple ground substitution σ; since Cσ is valid in I , Cσ is also valid.

We call the simple most general unifier σ that is computed during an inference ι and applied to the conclusion the pivotal substitution of ι. (For ground inferences, the pivotal substitution is the identity mapping.) If L is the literal

[¬] s ≈ t or [¬] s[u] ≈ t of
the second or only premise that is eliminated in ι, we call Lσ the pivotal literal of ι, and we call sσ or s[u]σ the pivotal term of ι. Lemma 7.2. Let ι be an HSP Base inference

C 1 abstr(C 0 σ) or C 2 C 1 abstr(C 0 σ)
from weakly abstracted premises with pivotal substitution σ. Let ι be a simple ground instance of ι of the form

C 1 τ C 0 στ or C 2 τ C 1 τ C 0 στ
Then there is a simple ground instance of abstr(C 0 σ) that has the form C 0 στ ∨E, where E is a (possibly empty) disjunction of literals s ≈ s, and each literal of E is smaller than the pivotal literal of ι .

As M ⊆ M implies R S Inf (M ) ⊆ R S Inf (M ), we obtain R S Inf (sgi(N )\sgi(N )) ⊆ R S Inf (sgi(N \N )). Furthermore, it is fairly easy to see that sgi(N )\(R S Cl (sgi(N ) ∪ GndTh(B)) ∪ GndTh(B)) ⊆ sgi(N \ R H Cl (N )).
Using these two results we can prove the following lemmas:

Lemma 7.3. R H = (R H Inf , R H Cl ) is a redundancy criterion with respect to |= B .
Lemma 7.4. Let N , N and M be sets of weakly abstracted clauses such that N ⊆ R H Cl (N ). If N is sufficiently complete, then so are N ∪ M and N \ N .

We now encode arbitrary term-generated Σ B -interpretation by sets of unit ground clauses in the following way: Let I ∈ B be a term-generated Σ B -interpretation. For every Σ B -ground term t let m(t) be the smallest ground term of the congruence class of t in I. We define a rewrite system E I by

E I = { t → m(t) | t ∈ T Σ , t = m(t) }.
Obviously, E I is right-reduced; since all rewrite rules are contained in , E I is terminating; and since every ground term t has m(t) as its only normal form, E I is also confluent. Now let E I be the set of all rules l → r in E I such that l is not reducible by E I \ {l → r}. Clearly every term that is reducible by E I is also reducible by E I ; conversely every term that is reducible by E I has a minimal subterm that is reducible by E I and the rule in E I that is used to rewrite this minimal subterm is necessarily contained in E I . Therefore E I and E I define the same set of normal forms, and from this we can conclude that E I and E I induce the same equality relation on ground Σ B -terms.

We identify E I with the set of clauses { t ≈ t | t → t ∈ E I }. Let D I be the set of all clauses t ≈ t , such that t and t are distinct ground Σ B -terms in normal form with respect to E I .12 Lemma 7.5. Let I ∈ B be a term-generated Σ B -interpretation and let C be a ground BG clause. Then C is true in I if and only if there exist clauses

C 1 , . . . , C n in E I ∪ D I such that C 1 , . . . , C n |= C and C C i for 1 ≤ i ≤ n.
Proof. The "if" part follows immediately from the fact that I |= E I ∪ D I . For the "only if" part assume that the ground BG clause C is true in I. Consequently, there is some literal s ≈ t or s ≈ t of C that is true in I. Then this literal follows from (i) the rewrite rules in E I that are used to normalize s to its normal form s , (ii) the rewrite rules in E I that are used to normalize t to its normal form t , and, in the case of a negated literal s ≈ t, (iii) the clause s ≈ t ∈ D I . It is routine to show that all these clauses are smaller than or equal to s ≈ t or s ≈ t, respectively, and hence smaller than or equal to C.

E I ∪ D I ∪ sgi(N ), it is in R S Cl (E I ∪ D I ∪ sgi(N )). Hence R S Inf (E I ∪ D I ∪ sgi(N ) ∪ GndTh(B)) ⊆ R S Inf (N I ).
A clause set N is called saturated (with respect to an inference system I and a redundancy criterion R) if ι ∈ R Inf (N ) for every inference ι with premises in N .

Theorem 7.8. Let I ∈ B be a term-generated Σ B -interpretation and let N be a set of weakly abstracted Σ-clauses. If I satisfies all BG clauses in sgi(N ) and N is saturated with respect to HSP Base and R H , then N I is saturated with respect to SSP and R S .

Proof. We have to show that every SSP-inference from clauses of N I is contained in R S Inf (N I ). We demonstrate this in detail for the equality resolution and the negative superposition rule. The analysis of the other rules is similar. Note that by Lemma 7.5 every BG clause that is true in I and is not contained in E I ∪ D I follows from smaller clauses in E I ∪ D I , thus it is in R S Cl (N I ); every inference involving such a clause is in R S Inf (N I ). The equality resolution rule is obviously not applicable to clauses from E I ∪ D I . Suppose that ι is an equality resolution inference with a premise Cσ, where C ∈ N and σ is a simple substitution and reduced with respect to E I . If Cσ is a BG clause, then ι is in R S Inf (N I ). If the pivotal term of ι is a pure BG term then the pivotal literal is pure BG as well. Because the pivotal literal is maximal in Cσ it follows from properties of the ordering that Cσ is a BG clause. Because we have already considered this case we can assume from now on that the pivotal term of ι is not pure BG and that Cσ is an FG clause. It follows that ι is a simple ground instance of a hierarchic inference

ι from C. Since ι is in R H Inf (N ), ι is in R S Inf (sgi(N ) ∪ GndTh(B))
, by Lemma 7.7, this implies again ι ∈ R S Inf (N I ). Obviously a clause from D I cannot be the first premise of a negative superposition inference. Suppose that the first premise is a clause from E I . The second premise cannot be a FG clause, since the maximal sides of maximal literals in a FG clause are reduced; as it is a BG clause, the inference is redundant. Now suppose that ι is a negative superposition inference with a first premise Cσ, where C ∈ N and σ is a simple substitution and reduced with respect to E I . If Cσ is a BG clause, then ι is in R S Inf (N I ). Otherwise, with the same arguments as for the equality resolution case above, the pivotal term is not pure BG and Cσ is a FG clause. Hence we can conclude that the second premise can be written as C σ, where C ∈ N is a FG clause (without loss of generality, C and C do not have common variables). If the overlap takes place below a variable occurrence, the conclusion of the inference follows from Cσ and some instance C ρ, which are both smaller than C σ. Otherwise, ι is a simple ground instance of a hierarchic inference ι from C. In both cases, ι is contained in R S Inf (N I ). The crucial property of abstracted clauses that is needed in the proof of this theorem is that there are no superposition inferences between clauses in E I and FG ground instances Cσ in N I , or in other words, that all FG terms occurring in ground instances Cσ are reduced w. r. t. E I . This motivates the definition of target terms in Def. 5.1: Recall that two different domain elements must always be interpreted differently in I and that a domain element is smaller in the term ordering than any ground term that is not a domain element. Consequently, any domain element is the smallest term in its congruence class, so it is reduced by E I . Furthermore, by the definition of N I , ζσ is reduced by E I for every variable ζ. So variables and domain elements never need to be abstracted out. Other BG terms (such as parameters α or non-constant terms ζ 1 + ζ 2 ) have to be abstracted out if they occur below a FG operator, or if one of their sibling terms is a FG term or an impure BG term (since σ can map the latter to a FG term). On the other hand, abstracting out FG terms as in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] is never necessary to ensure that FG terms are reduced w. r. t. E I .

If N is saturated with respect to HSP Base and R H and does not contain the empty clause, then Close cannot be applicable to N . If (Σ B , B) is compact, this implies that there is some term-generated Σ B -interpretation I ∈ B that satisfies all BG clauses in sgi(N ). Hence, by Thm. 7.8, the set of reduced simple ground instances of N has a model that also satisfies E I ∪ D I . Sufficient completeness allows us to show that this is in fact a model of all ground instances of clauses in N and that I is its restriction to Σ B : Theorem 7.9. If the BG specification (Σ B , B) is compact, then HSP Base and R H are statically refutationally complete for all sufficiently complete sets of clauses, i. e., if a set of clauses N is sufficiently complete and saturated w. r. t. HSP Base and R H , and N |= B , then ∈ N .

Proof. Let N be a set of weakly abstracted clauses that is sufficiently complete, and saturated w. r. t. the hierarchic superposition calculus and R H and does not contain . Consequently, the Close rule is not applicable to N . By compactness, this means that the set of all Σ B -clauses in sgi(N ) is satisfied by some termgenerated Σ B -interpretation I ∈ B. By Thm. 7.8, N I is saturated with respect to the standard superposition calculus. Since / ∈ N I , the refutational completeness of standard superposition implies that there is a Σ-model I of N I . Since N is sufficiently complete, we know that for every ground term t of a BG sort there exists a BG term t such that t ≈ t is true in I . Consequently, for every ground instance of a clause in N there exists an equivalent simple ground instance, thus I is also a model of all ground instances of clauses in N . To see that the restriction of I to Σ B is isomorphic to I and thus in B, note that I satisfies E I ∪ D I , preventing confusion, and that N is sufficiently complete, preventing junk. Since I satisfies N and I | ΣB ∈ B, we have N |= B A theorem proving derivation D is a finite or infinite sequence of weakly abstracted clause sets N 0 , N 1 , ..., such that N i and N i+1 are equisatisfiable w. r. t.

|= B and N i \ N i+1 ⊆ R H Inf (N i+1
) for all indices i. The set N ∞ = i≥0 j≥i N j is called the limit of D; the set N ∞ = i≥0 N i is called the union of D. It is easy to show that every clause in N ∞ is either contained in N ∞ or redundant w. r. t. N ∞ . The derivation D is said to be fair, if every HSP Base -inference with (non-redundant) premises in N ∞ becomes redundant at some point of the derivation. The limit of a fair derivation is saturated [START_REF] Bachmair | Resolution Theorem Proving[END_REF]; this is the key result that allows us to deduce dynamic refutational completeness from static refutational completeness:

Theorem 7.10. If the BG specification (Σ B , B) is compact, then HSP Base and R H are dynamically refutationally complete for all sufficiently complete sets of clauses, i. e., if N |= B , then every fair derivation starting from abstr(N ) eventually generates .

In the rest of the paper, we consider only theorem proving derivations where each set N i+1 results from from N i by either adding the conclusions of inferences from N i , or by deleting clauses that are redundant w. r. t. N i+1 , or by applying the following generic simplification rule for clause sets: Notice, though, that impure BG terms or FG terms can in general not be simplified by BG tautologies. Although, e. g., f(X) + 1 ≈ y + 1 is larger than 1 + f(X) ≈ y + 1 (with a LPO), such a "simplification" is not justified by the redundancy criterion. Indeed, in the example it destroys sufficient completeness.

Simp N ∪ {C} N ∪ {D 1 , . . . , D n } if n ≥ 0 and (i) D i is weakly abstracted, for all i = 1, . . . , n, (ii) N ∪ {C} |= B D i , and (iii) C ∈ R H Cl (N ∪ {D 1 , . . . , D n }). Condition (ii)
We have to point out a limitation of the calculus described above. The standard superposition calculus SSP exists in two variants: either using the Equality factoring rule, or using the Factoring and Merging paramodulation rules. Only the first of these variants works together with weak abstraction. Consider the following example. Let

N = { α + β ≈ α, c ≈ β ∨ c ≈ 0, c ≈ β ∨ c ≈ 0 }.
All clauses in N are weakly abstracted. Since the first clause entails β ≈ 0 relative to linear arithmetic, the second and the third clause are obviously contradictory. The HSP Base calculus as defined above is able to detect this by first applying Equality factoring to the third clause, yielding c ≈ 0 ∨ β ≈ 0, followed by two Negative superposition steps and Close. If Equality factoring is replaced by Factoring and Merging paramodulation, however, the refutational completeness of HSP Base is lost. The only inference that remains possible is a Negative superposition inference between the third and the second clause. But since the conclusion of this inference is a tautology, the inference is redundant, so the clause set is saturated. (Note that the clause β ≈ 0 is entailed by N , but it is not explicitly present, so there is no way to perform a Merging paramodulation inference with the smaller side of the maximal literal of the third clause.)

Local Sufficient Completeness

The definition of sufficient completeness w. r. t. simple instances that was given in Sect. 3 requires that every ground BG-sorted FG term s is equal to some ground BG term t in every Σ-model J of sgi(N ) ∪ GndTh(B). It is rather evident, however, that this condition is sometimes stronger than needed. For instance, if the set of input clauses N is ground, then we only have to consider the ground BG-sorted FG terms that actually occur in N [START_REF] Kruglov | Superposition decides the first-order logic fragment over ground theories[END_REF] (analogously to the Nelson-Oppen combination procedure). A relaxation of sufficient completeness that is also useful for non-ground clauses and that still ensures refutational completeness was given by Kruglov [START_REF] Kruglov | Superposition Modulo Theory[END_REF]: Definition 8.1 (Smooth ground instance). We say that a substitution σ is smooth if for every variable ζ ∈ dom(σ) all BG-sorted (proper or non-proper) subterms of ζσ are pure BG terms. If F σ is a ground instance of a term or clause F and σ is smooth, F σ is called a smooth ground instance. (Recall that every ground BG term is necessarily pure.) If N is a set of clauses, smgi(N ) denotes the set of all smooth ground instances of clauses in N .

Every smooth substitution is a simple substitution, but not vice versa. For instance, if x is a FG-sorted variable and y is an ordinary BG-sorted variable, then σ 1 = [x → cons(f(1) + 2, empty)] and σ 2 = [y → f(1)] are simple substitutions, but neither of them is smooth, since xσ 1 and yσ 2 contain the BG-sorted FG subterm f(1).

Definition 8.2 (Local sufficient completeness).

Let N be a Σ-clause set. We say that N is locally sufficiently complete w. r. t. smooth instances if for every Σ B -interpretation I ∈ B, every Σ-model J of sgi(N ) ∪ E I ∪ D I , and every BG-sorted FG term s occurring in smgi(N ) \ R S Cl (smgi(N ) ∪ E I ∪ D I ) there is a ground BG term t such that J |= s ≈ t. (Again, we will from now on omit the phrase "w. r. t. smooth instances" for brevity.) Example 8.3. The clause set N = { X ≈ α ∨ f(X) ≈ β } is locally sufficiently complete: The smooth ground instances have the form s ≈ α ∨ f(s ) ≈ β, where s is a pure BG term. We have to show that f(s ) equals some ground BG term t whenever the smooth ground instance is not redundant. Let I ∈ B be a Σ Binterpretation and J be a Σ-model of sgi(N )

∪ E I ∪ D I . If I |= s ≈ α, then s ≈ α follows from some clauses in E I ∪ D I , so s ≈ α ∨ f(s ) ≈ β is contained in R S
Cl (smgi(N ) ∪ E I ∪ D I ) and f(s ) need not be considered. Otherwise I |= s ≈ α, then f(s ) occurs in a non-redundant smooth ground instance of a clause in N and J |= f (s ) ≈ β, so t := β has the desired property. On the other hand, N is clearly not sufficiently complete, since there are models of sgi(N ) ∪ GndTh(B) in which f(β) is interpreted by some junk element that is different from the interpretation of any ground BG term.

The example demonstrates that local sufficient completeness is significantly more powerful than sufficient completeness, but this comes at a price. For instance, as shown by the next example, local sufficient completeness is not preserved by abstraction: Example 8.4. Suppose that the BG specification is linear integer arithmetic (including parameters α, β, γ), the FG operators are f : int → int, g : int → data, a : → data, the term ordering is an LPO with precedence g > f > a > γ > β > α > 3 > 2 > 1, and the clause set N is given by

γ ≈ 1 (1) f(2) ≈ 2 (4) g(f(α)) ≈ a ∨ g(f(β)) ≈ a (6) β ≈ 2 (2) f(3) ≈ 3 (5) g(f(α)) ≈ a ∨ g(f(β)) ≈ a (7) α ≈ 3 (3) g(f(γ)) ≈ a ∨ g(f(β)) ≈ a (8)
Since all clauses in N are ground, smgi(N ) = sgi(N ) = N . Clause ( 8) is redundant w. r. t. smgi(N ) ∪ E I ∪ D I (for any I): it follows from clauses ( 6) and ( 7), and both are smaller than [START_REF] Baumgartner | ME(LIA) -Model Evolution With Linear Integer Arithmetic Constraints[END_REF]. The BG-sorted FG terms in non-redundant clauses are f(2), f(3), f(α), and f(β), and in any Σ-model J of sgi(N ) ∪ E I ∪ D I , these are necessarily equal to the BG terms 2 or 3, respectively, so N is locally sufficiently complete.

Let N = abstr(N ), let I be a BG-model such that E I contains α ≈ 3, β ≈ 2, and γ ≈ 1 (among others), D I contains 1 ≈ 2, 1 ≈ 3, and 2 ≈ 3 (among others), and let J be a Σ-model of sgi(N ) ∪ E I ∪ D I in which f(1) is interpreted by some junk element. The set N contains the clause g(f(X)) ≈ a ∨ g(f(Y )) ≈ a ∨ γ ≈ X ∨ β ≈ Y obtained by abstraction of [START_REF] Baumgartner | ME(LIA) -Model Evolution With Linear Integer Arithmetic Constraints[END_REF]. Its smooth ground instance

C = g(f(1)) ≈ a ∨ g(f(2)) ≈ a ∨ γ ≈ 1 ∨ β ≈ 2 is not redundant: it follows from other clauses in smgi(N ) ∪ E I ∪ D I , namely α ≈ 3 (3) g(f(3)) ≈ a ∨ g(f(2)) ≈ a ∨ α ≈ 3 ∨ β ≈ 2 (6 ) g(f(3)) ≈ a ∨ g(f(2)) ≈ a ∨ α ≈ 3 ∨ β ≈ 2 (7 )
but the ground instances (6 ) and (7 ) that are needed here are larger than C. Since C contains the BG-sorted FG term f(1) which is interpreted differently from any BG term in J, N is not locally sufficiently complete.

Local sufficient completeness of a clause set suffices to ensure refutational completeness. Kruglov's proof [START_REF] Kruglov | Superposition Modulo Theory[END_REF] works also if one uses weak abstraction instead of strong abstraction and ordinary as well as abstraction variables, but it relies on an additional restriction on the term ordering. 13 We give an alternative proof that works without this restriction.

The proof is based on a transformation on Σ-interpretations. Let J be an arbitrary Σ-interpretation. We transform J into a term-generated Σ-interpretation nojunk(J) without junk in two steps. In the first step, we define a Σ-interpretation J as follows:

-For every FG sort ξ, define J ξ = J ξ .

-For every BG sort ξ, define

J ξ = { t J | t is a ground BG term of sort ξ }. -For every f : ξ 1 . . . ξ n → ξ 0 the function J f : J ξ1 × • • • × J ξn → J ξ0 maps (a 1 , . . . , a n ) to J f (a 1 , . . . , a n ), if J f (a 1 , . . . , a n ) ∈ J ξ0
, and to an arbitrary element of J ξ0 otherwise.

That is, we obtain J from J be deleting all junk elements from J ξ if ξ is a BG sort, and by redefining the interpretation of f arbitrarily whenever J f (a 1 , . . . , a n ) is a junk element.

In the second step, we define the Σ-interpretation nojunk(J) = J as the term-generated subinterpretation of J , that is,

-For every sort ξ, J ξ = { t J | t is a ground term of sort ξ }, -For every f : ξ 1 . . . ξ n → ξ 0 , the function J f : J ξ1 × • • • × J ξn → J ξ0 satisfies J f (a 1 , . . . , a n ) = J f (a 1 , . . . , a n ).
Lemma 8.5. Let J, J , and nojunk(J) = J be given as above. Then the following properties hold:

(i) t J = t J for every ground term t.

(ii) J ξ = J ξ for every BG sort ξ.

(iii) J is a term-generated Σ-interpretation and J | ΣB is a term-generated Σ B -interpretation. (iv) If t = f (t 1 , . . . , t n ) is ground, t J i = t J i for all i, and t J ∈ J ξ , then t J = t J . (v) If t is ground and all BG-sorted subterms of t are BG terms, then

t J = t J . (vi) If C is a ground BG clause, then J |= C if and only if J |= C if and only if J | ΣB |= C.
Proof. Properties (i)-(iv) follow directly from the definition of J and J . Property (v) follows from (iv) and the definition of J by induction over the term structure. By (i) and (v), every ground BG term is interpreted in the same way in J and J , moreover it is obvious that every ground BG term is interpreted in the same way in J and J | ΣB ; this implies (vi).

Lemma 8.6. If J is a Σ-interpretation and I = nojunk(J), then for every ground term s there exists a ground term t such that s I = t I and all BG-sorted (proper or non-proper) subterms of t are BG terms.

Proof. If s has a BG sort ξ, then this follows directly from the fact that s I ∈ I ξ and that every element of I ξ equals t I for some ground BG term t of sort ξ. Proof. Let J be defined as above, then (tτ ) J = (tτ ) J for any term t occurring in C by Lemma 8.5-(i). We prove that (tτ ) J = (tτ ) J by induction over the term structure: If t is a variable, then by smoothness all BG-sorted subterms of tτ are BG terms, hence (tτ ) J = (tτ ) J by . Otherwise let t = f (t 1 , . . . , t n ). If tτ is a BG term, then again (tτ ) J = (tτ ) J by Lemma 8.5-(v). If tτ is a FG term of sort ξ, then t must be a FG term of sort ξ as well. By the induction hypothesis, (t i τ ) J = (t i τ ) J for every i. If ξ is a FG sort, then trivially (tτ ) J = J f ((t 1 τ ) J , . . . , (t n τ ) J ) is contained in J ξ , so (tτ ) J = (tτ ) J by Lemma 8.5-(iv). Otherwise, tτ is a BG-sorted FG term occurring in smgi(N ) \ R S Cl (smgi(N ) ∪ E I ∪ D I ). By local sufficient completeness, there exists a ground BG term s such that s J = (tτ ) J , hence (tτ ) J ∈ J ξ . Again, Lemma 8.5-(iv) yields (tτ ) J = (tτ ) J .

If
Since all left and right-hand sides of equations in Cτ are evaluated in the same way in J and J, it follows that J |= Cτ if and only if J |= Cτ . Lemma 8.9. Let N be a set of Σ-clauses that is locally sufficiently complete. Let I ∈ B be a Σ B -interpretation, let J be a Σ-model of sgi(N ) ∪ E I ∪ D I , and let J = nojunk(J). Then J is a model of N .

Proof. The proof proceeds in three steps. In the first step we show that J is a model of smgi(N ) \ R S Cl (smgi(N ) ∪ E I ∪ D I ): Let C ∈ N and let Cτ be a smooth ground instance in smgi(N ) \ R S Cl (smgi(N ) ∪ E I ∪ D I ). Since every smooth ground instance is a simple ground instance and J is a Σ-model of sgi(N ), we know that J |= Cτ . By Lemma 8.8, this implies J |= Cτ .

In the second step we show that J is a model of smgi(N ). Since we already know that J is a model of smgi

(N ) \ R S Cl (smgi(N ) ∪ E I ∪ D I ), it is clearly sufficient to show that J is a model of R S Cl (smgi(N ) ∪ E I ∪ D I ):
∪ E I ∪ D I )\R S Cl (smgi(N ) ∪ E I ∪ D I ) |= R S Cl (smgi(N ) ∪ E I ∪ D I ). So J is a model of R S Cl (smgi(N ) ∪ E I ∪ D I ).
We can now show the main statement: We know that J is a term-generated Σ-interpretation, so J |= N holds if and only if J is a model of all ground instances of clauses in N . Let Cσ be an arbitrary ground instance of C ∈ N . By Cor. 8.7, there is a smooth ground instance Cτ such that J |= Cσ if and only if J |= Cτ . As the latter has been shown in the second step, the result follows.

Theorem 8.10. If the BG specification (Σ B , B) is compact and if the clause set N is locally sufficiently complete, then HSP Base and R H are dynamically refutationally complete for abstr(N ), i. e., if N |= B , then every fair derivation starting from abstr(N ) eventually generates .

Proof. Let D = (N i ) i≥0 be a fair derivation starting from N 0 = abstr(N ), and let N ∞ be the limit of D. By fairness, N ∞ is saturated w. r. t. HSP Base and R H . If / ∈ N ∞ , then the Close rule is not applicable to N ∞ . Since (Σ B , B) is compact, this means that the set of all Σ B -clauses in sgi(N ∞ ) is satisfied by some term-generated Σ B -interpretation I ∈ B. By Thm. 7.8, (N ∞ ) I is saturated with respect to the standard superposition calculus. Since / ∈ (N ∞ ) I , the refutational completeness of standard superposition implies that there is a Σ-model J of (N ∞ ) I , and since E I ∪ D I ⊆ (N ∞ ) I , J is also a Σ-model of sgi(N ∞ ) ∪ E I ∪ D I . Since every clause in N 0 is either contained in N ∞ or redundant w. r. t. N ∞ , every simple ground instance of a clause in N 0 is a simple ground instance of a clause in N ∞ or contained in GndTh(B) or redundant w. r. t. sgi(N ∞ ) ∪ GndTh(B). We conclude that J is a Σ-model of sgi(N 0 ), and since sgi(N 0 ) and sgi(N ) are equivalent, J is a Σ-model of sgi(N ). Now define J = nojunk(J). By Lemma 8.5, J is a term-generated Σ-interpretation, J | ΣB is a term-generated Σ B -interpretation, and J | ΣB satisfies E I ∪ D I . Consequently, J | ΣB is isomorphic to I and thus contained in B. Finally, J is a model of N by Lemma 8.9.

If all BG-sorted FG terms in a set N of clauses are ground, local sufficient completeness can be established automatically by adding a "definition" of the form t ≈ α, where t is a ground BG-sorted FG term and α is a parameter. The following section explains this idea in a more general way.

Local Sufficient Completeness by Define

The HSP Base inference system will derive a contradiction if the input clause set is inconsistent and (locally) sufficiently complete (cf. Sect. 8). In this section we extend this functionality by adding an inference rule, Define, which can turn input clause sets that are not sufficiently complete into locally sufficiently complete ones. Technically, the Define rule derives "definitions" of the form t ≈ α, where t is a ground BG-sorted FG term and α is a parameter of the proper sort. For economy of reasoning, definitions are introduced only on a by-need basis, when t appears in a current clause, and t ≈ α is used to simplify that clause immediately.

We need one more preliminary definition before introducing Define formally.

(N ) = { unabstr(C) | C ∈ N }.
The full inference system HSP of the hierarchic superposition calculus consists of the inference rules of HSP Base and the following Define inference rule. As for the other inference rules we suppose that all premises are weakly abstracted. In (i), by minimality we mean that no proper subterm of t[ζ 1 , . . . , ζ n ] is a BG-sorted non-variable term with a toplevel FG operator. In effect, the Define rule eliminates such terms inside-out. Conditions (iii) and (iv) are needed for soundness. Condition (v) is needed to guarantee that Define is a simplifying inference rule, much like the Simp rule in Sect. 7. 14 In particular, it makes sure that Define cannot be applied to definitions themselves. Proof. For the inference rules of HSP Base , the result follows from Thm. 6.1.

Define N ∪ {L[t[ζ 1 , . . . , ζ n ]] ∨ D} N ∪ abstr({t[t 1 , . . . , t n ] ≈ α t[t1,...,tn] , L[α t[t1,...,tn] ] ∨ D} if (i) t[ζ 1 , . . . ,
For Define, we observe first that condition (ii) implies that

L[t[ζ 1 , . . . , ζ n ]] ∨ D and L[t[t 1 , . . . , t n ]] ∨ D are equivalent. If N ∪ {L[t[t 1 , . . . , t n ]] ∨ D} is B- satisfiable, let I be a Σ-model of all ground instances of N ∪ {L[t[t 1 , . . . , t n ]]∨D} such that I| ΣB is in B.
By condition (iii), t[t 1 , . . . , t n ] is ground. Let J be the Σ-interpretation obtained from J by redefining the interpretation of α t[t1,...,tn] in such a way that α J t[t1,...,tn] = t[t 1 , . . . , t n ] I , then J is a Σ-model of every ground instance of N , t[t 1 , . . . , t n ] ≈ α t[t1,...,tn] and L[α t[t1,...,tn] ] ∨ D, and hence also a model of the abstractions of these clauses. Conversely, every model of

t[t 1 , . . . , t n ] ≈ α t[t1,...,tn] and L[α t[t1,...,tn] ] ∨ D is a model of L[t[t 1 , . . . , t n ]] ∨ D. Example 9.3. Let C = g(f(x, y) + 1, x, y) ≈ 1 ∨ x ≈ 1 + β ∨ y ≈ c be the premise of a Define inference. We get unabstr(C) = g(f(1 + β, c) + 1, 1 + β, c) ≈ 1. The (unabstracted) conclusions are the definition f(1 + β, c) ≈ α f(1+β,c) and the clause g(α f(1+β,c) + 1, x, y) ≈ 1 ∨ x ≈ 1 + β ∨ y ≈ c. Abstraction yields f(X, c) ≈ α f(1+β,c) ∨ X ≈ 1 + β and g(Z, x, y) ≈ 1 ∨ x ≈ 1 + β ∨ y ≈ c ∨ Z ≈ α f(1+β,c) + 1.
One might be tempted to first unabstract the premise C before applying Define. However, unabstraction may eliminate FG terms (c in the example) which is not undone by abstraction. This may lead to incompleteness. Example 9.5. Consider the weakly abstracted clauses P(0), f(x) > 0 ∨ ¬P(x), Q(f(x)), ¬Q(x) ∨ 0 > x. Suppose ¬P(x) is maximal in the second clause. By superposition between the first two clauses we derive f(0) > 0. With Define we obtain f(0) ≈ α f(0) and α f(0) > 0, the latter replacing f(0) > 0. From the third clause and f(0) ≈ α f(0) we obtain Q(α f(0) ), and with the fourth clause 0 > α f(0) . Finally we apply Close to {α f(0) > 0, 0 > α f(0) }.

It is easy to generalize Thm. 8.10 to the case that local sufficient completeness does not hold initially, but is only established with the help of Define inferences: Theorem 9.6. Let D = (N i ) i≥0 be a fair HSP derivation starting from N 0 = abstr(N ), let k ≥ 0, such that N k = abstr(N ) and N is locally sufficiently complete. If the BG specification (Σ B , B) is compact, then the limit of D contains if and only if N is B-unsatisfiable.

Proof. Since every derivation step in an HSP derivation is satisfiability-preserving, the "only if" part is again obvious. For the "if" part, we assume that N ∞ , the limit of D, does not contain . By fairness, N ∞ is saturated w. r. t. HSP and R H . We start by considering the subderivation (N i ) i≥k starting with N k = abstr(N ). Like in the proof of Thm. 8.10, we can show that N is B-satisfiable, that is, there exists a model J of N that is a term-generated Σ-interpretation, and whose restriction J| ΣB is contained in B. From Lemma 7.1 and Prop. 5.2 we see that N |= B N k , and similarly N 0 |= B N . Furthermore, since every clause in N 0 \ N k must be redundant w. r. t. N k , we have N k |= B N 0 . Combining these three entailments, we conclude that N |= B N , so N is B-satisfiable and J is a model of N .

Condition (v) of the Define rule requires that the clause that is deleted during a Define inference must be redundant with respect to the remaining clauses. This condition is needed to preserve refutational completeness. There are cases, however, where condition (v) prevents us from introducing a definition for a subterm. Consider the clause set N = {C} where C = f(c) ≈ 1 ∨ c ≈ d, the constants c and d are FG-sorted, f is a BG-sorted FG operator, and c d 1.

The literal f(c) ≈ 1 is maximal in C. The clause set N = abstr(N ) is not locally sufficient complete (the BG-sorted FG-term f(c) may be interpreted differently from all BG terms in a Σ-model). Moreover, it cannot be made locally sufficient complete using the Define rule, since the definition f(c) ≈ α f(c) is larger w. r. t. the clause ordering than C, in violation of condition (v) of Define.

However, at the beginning of a derivation, we may be a bit more permissive. Let us define the reckless Define inference rule in the same way as the Define rule except that the applicability condition (v) is dropped. Clearly, in the example above, the reckless Define rule allows us to derive the locally sufficiently complete clause set

N = {α f(c) ≈ 1 ∨ c ≈ d, f(c) ≈ α f(c) } as desired.
In fact, we can show that this is always possible if N is a finite clause set in which all BG-sorted FG terms are ground. Definition 9.7 (Pre-derivation). Let N 0 be a weakly abstracted clause set. A pre-derivation (of a clause set N pre ) is a derivation of the form N 0 , N 1 , . . . , (N k = N pre ), for some k ≥ 0, with the inference rule reckless Define only, and such that each clause C ∈ N pre either does not contain any BG-sorted FG operator or C = abstr(C ) and C is a definition, i. e., a ground positive unit clause of the form f(t 1 , . . . , t n ) ≈ t where f is a BG-sorted FG operator, t 1 , . . . , t n do not contain BG-sorted FG operators, and t is a background term. Lemma 9.8. Let N be a finite clause set in which all BG-sorted FG terms are ground. Then there is a pre-derivation starting from N 0 = abstr(N ) such that N pre is locally sufficiently complete.

Proof. Since every term headed by a BG-sorted FG operator in unabstr(N 0 ) is ground, we can incrementally eliminate all occurrences of terms headed by BGsorted FG operators from N 0 , except those in abstractions of definitions. Let N 0 , N 1 , . . . , (N k = N pre ) be the sequence of sets of clauses obtained in this way. We will show that N pre is locally sufficiently complete.

Let I ∈ B be a Σ B -interpretation, let J be a Σ-model of sgi(N pre ) ∪ E I ∪ D I and let Cθ be a smooth ground instance in smgi(N ) \ R S Cl (smgi(N ) ∪ E I ∪ D I ).

We have to show that for every BG-sorted FG term s occurring in Cθ there is a ground BG term t such that J |= s ≈ t.

If C does not contain any BG-sorted FG operator, then there are no BGsorted FG terms in Cθ, so the property is vacuously true. Otherwise C = abstr(C ) and C is a definition f(t 1 , . . . , t n ) ≈ t where f is a BG-sorted FG operator, t 1 , . . . , t n do not contain BG-sorted FG operators, and t is a background term. In this case, C must have the form f(u 1 , . . . , u n ) ≈ u ∨ E, such that E is a BG clause, u 1 , . . . , u n do not contain BG-sorted FG operators, and u is a BG term. The only BG-sorted FG term in the smooth instance Cθ is therefore f(u 1 θ, . . . , u n θ). If any literal of Eθ were true in J, then it would follow from E I ∪ D I , therefore Cθ ∈ R S Cl (smgi(N ) ∪ E I ∪ D I ), contradicting the assumption. Hence J |= f(u 1 θ, . . . , u n θ) ≈ uθ, and since uθ is a ground BG term, the requirement is satisfied. Lemma 9.8 will be needed to prove a completeness result for the fragment defined in the next section.

10 The Ground BG-sorted Term Fragment According to Thm. 8.10, the HSP Base calculus is refutationally complete provided that the clause set is locally sufficiently complete and the BG specification is compact. We have seen in the previous section that the (reckless) Define rule can help to establish local sufficient completeness by introducing new parameters. In fact, finite clause sets in which all BG-sorted FG terms are ground can always be converted into locally sufficiently complete clause sets (cf. Lemma 9.8). On the other hand, as noticed in Sect. 3, the introduction of parameters can destroy the compactness of the BG specification. In this and the following section, we will identify two cases where we can not only establish local sufficient completeness, but where we can also guarantee that compactness poses no problems. The ground BG-sorted term fragment (GBT fragment) is one such case: Definition 10.1 (GBT fragment). A clause C is a GBT clause if all BGsorted terms in C are ground. A finite clause set N belongs to the GBT fragment if all clauses in N are GBT clauses.

Clearly, by Lemma 9.8 for every clause set N that belongs to the GBT fragment there is a pre-derivation that converts abstr(N ) into a locally sufficiently complete clause set. Moreover, pre-derivations also preserve the GBT property: Lemma 10.2. If unabstr(N ) belongs to the GBT fragment and N is obtained from N by a reckless Define inference, then unabstr(N ) also belongs to the GBT fragment.

The proof can be found in [START_REF] Baumgartner | Hierarchic superposition revisited[END_REF].

As we have seen, N pre is locally sufficiently complete. At this stage this suggests to exploit the completeness result for locally sufficiently complete clause sets, Thm. 8.10. However, Thm. 8.10 requires compact BG specifications, and the question is if we can avoid this. We can indeed get a complete calculus under rather mild assumptions on the Simp rule: Definition 10.3 (Suitable Simp inference). Let fin be a strict partial term ordering such that for every ground BG term s only finitely many ground BG terms t with s fin t exist. 15 We say that a Simp inference with premise N ∪ {C} and conclusion N ∪ {D} is suitable (for the GBT fragment) if (i) for every BG term t occurring in unabstr(D) there is a BG term s ∈ unabstr(C) such that s fin t, (ii) every occurrence of a BG-sorted FG operator f in unabstr(D) is of the form f(t 1 , . . . , t n ) ≈ t where t is a ground BG term, (iii) every BG term in D is pure, and (iv) if every BG term in unabstr(C) is ground then every BG term in unabstr(D) is ground.

We say the Simp inference rule is suitable if every Simp inference is.

Expected simplification techniques like demodulation, subsumption deletion and evaluation of BG subterms are all covered as suitable Simp inferences. Also, evaluation of BG subterms is possible, because simplifications are not only decreasing w. r. t. but additionally also decreasing w. r. t. fin , as expressed in condition (i). Without it, e. g., the clause P(1+1, 0) would admit infinitely many simplified versions P(2, 0), P(2, 0 + 0), P(2, 0 + (0 + 0)), etc.

The HSP Base inferences do in general not preserve the shape of the clauses in unabstr(N pre ); they do preserve a somewhat weaker property -cleannesswhich is sufficient for our purposes. Definition 10.4 (Clean clause). A weakly abstracted clause C is clean if (i) every BG term in C is pure, (ii) every BG term in unabstr(C) is ground, and (iii) every occurrence of a BG-sorted FG operator f in unabstr(C) is in a positive literal of the form f(t 1 , . . . , t n ) ≈ t where t is a ground BG term.

For example, if c is FG-sorted, then P(f(c) + 1) is not clean, while f(x) ≈ 1 + α ∨ P(x) is. A clause set is called clean if every clause in N is. Notice that N pre is clean. The proof can be found in [START_REF] Baumgartner | Hierarchic superposition revisited[END_REF]. Thanks to conditions (ii)-(iv) in Def. 10.3, suitable Simp inferences preserves cleanness: With the above lemmas we can prove our main result:

Theorem 10.7. The HSP calculus with a suitable Simp inference rule is dynamically refutationally complete for the ground BG-sorted term fragment. More precisely, let N be a finite set of GBT clauses and D = (N i ) i≥0 a fair HSP derivation such that reckless Define is is applied only in a pre-derivation (N 0 = abstr(N )), . . . , (N k = N pre ), for some k ≥ 0. Then the limit of D contains if and only if N is B-unsatisfiable.

Notice that Thm. 10.7 does not appeal to compactness of BG specifications.

Proof. Our goal is to apply Thm. 9.6 and its proof, in a slightly modified way. For that, we first need to know that N pre = abstr(N ) for some clause set N that is locally sufficiently complete.

We are given that N is a set of GBT clauses. Recall that weak abstraction (recursively) extracts BG subterms by substituting fresh variables and adding disequations. Unabstraction reverses this process (and possibly eliminates additional disequations). It follows that with N being a set of GBT clauses, so is unabstr(abstr(N )) = unabstr(N 0 ). From Lemma 10.2 it follows that unabstr(N pre ) is also a GBT clause set. Now chose N as the clause set that is obtained from N pre by replacing every clause C ∈ N pre such that unabstr(C) is a definition by unabstr(C). By construction of definitions, unabstraction reverses weak abstraction of definitions. It follows N pre = abstr(N ). By definition of pre-derivations, all BG-sorted FG terms occurring in unabstr(N pre ) occur in definitions. Hence, with unabstr(N pre ) being a set of GBT clauses so is N . It follows easily that N is locally sufficiently complete, as desired.

We cannot apply Thm. 9.6 directly now because it requires compactness of the BG specification, which cannot be assumed. However, we can use the following argumentation instead.

Let N ∞ = i≥0 N i be the union of D. We next show that unabstr(N ∞ ) contains only finitely many different BG terms and each of them is ground. Recall that unabstr(N pre ) is a GBT clause set, and so every BG term in unabstr(N pre ) is ground. Because Define is disabled in D, only HSP Base and (suitable) Simp inferences need to be analysed. Notice that N pre is clean and both the HSP Base and Simp inferences preserve cleanness, as per Lemmas 10.5-(1) and 10.6, respectively.

With respect to HSP Base inferences, together with Def. 10.4-(ii) it follows that every BG term t in the unabstracted version unabstr(C) of the inference conclusion C is ground. Moreover, t also occurs in the unabstracted version of some premise clause by . In other words, HSP Base inferences do not grow the set of BG terms w. r. t. unabstracted premises and conclusions With respect to Simp inferences, unabstr(N pre ) provide an upper bound w. r. t. the term ordering fin for all BG terms generated in Simp inferences. There can be only finitely many such terms, and each of them is ground, which follows from Def. 10.3-(i).

Because every BG term occurring in unabstr(N ∞ ) is ground, every BG clause in unabstr(N ∞ ) is a multiset of literals of the form s ≈ t or s ≈ t, where s and t are ground BG terms. With only finitely many BG terms available, there are only finitely many BG clauses in unabstr(N ∞ ), modulo equivalence. Because unabstraction is an equivalence transformation, there are only finitely many BG clauses in N ∞ as well, modulo equivalence.

Let N ∞ = i≥0 j≥i N j be the limit clause set of the derivation D, which is saturated w. r. t. the hierarchic superposition calculus and R H . Because D is not a refutation, it does not contain . Consequently the Close rule is not applicable to N ∞ . The set N ∞ , and hence also N ∞ ⊆ N ∞ , contains only finitely many BG clauses, modulo equivalence. This entails that the set of all Σ B -clauses in sgi(N ∞ ) is satisfied by some term-generated Σ B -interpretation I ∈ B. Now, the rest of the proof is literally the same as in the proof of Thm. 9.6.

Because unabstraction can also be applied to fully abstracted clauses, it is possible to equip the hierarchic superposition calculus of [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] with a correspondingly modified Define rule and get Thm. 10.7 in that context as well.

Kruglov and Weidenbach [START_REF] Kruglov | Superposition decides the first-order logic fragment over ground theories[END_REF] have shown how to use hierarchic superposition as a decision procedure for ground clause sets (and for Horn clause sets with constants and variables as the only FG terms). Their method preprocesses the given clause set by "basification", a process that removes BG-sorted FG terms similarly to our reckless Define rule. The resulting clauses then are fully abstracted and hierarchic superposition is applied. Some modifications of the inference rules make sure derivations always terminate. Simplification is restricted to subsumption deletion. The fragment of [START_REF] Kruglov | Superposition decides the first-order logic fragment over ground theories[END_REF] is a further restriction of the GBT fragment. We expect we can get decidability results for that fragment with similar techniques.

Linear Arithmetic

For the special cases of linear integer arithmetic (LIA) and linear rational arithmetic as BG specifications, the result of the previous section can be extended significantly: In addition to ground BG-sorted terms, we can also permit BGsorted variables and, in certain positions, even variables with offsets.

Recall that we have assumed that equality is the only predicate symbol in our language, so that a non-equational atom, say s < t, is to be taken as a shorthand for the equation (s < t) ≈ true. We refer to the terms that result from this encoding of atoms as atom terms; other terms are called proper terms.

Theorem 11.1. Let N be a set of clauses over the signature of linear integer arithmetic (with parameters α, β, etc.), such that every proper term in these clauses is either (i) ground, or (ii) a variable, or (iii) a sum ζ + k of a variable ζ and a number k ≥ 0 that occurs on the right-hand side of a positive literal s < ζ +k. If the set of ground terms occurring in N is finite, then N is satisfiable in LIA over Z if and only if N is satisfiable w. r. t. the first-order theory of LIA.

Proof. Let N be a set of clauses with the required properties, and let T be the finite set of ground terms occurring in N . We will show that N is equivalent to some finite set of clauses over the signature of linear integer arithmetic, which implies that it is satisfiable in the integer numbers if and only if it is satisfiable in the first-order theory of LIA.

In a first step, we replace every negative ordering literal ¬s < t or ¬s ≤ t by the equivalent positive ordering literal t ≤ s or t < s. All literals of clauses in the resulting set N 0 have the form s ≈ t, s ≈ t, s < t, s ≤ t, or s < ζ + k, where s and t are either variables or elements of T and k ∈ N. Note that the number of variables in clauses in N 0 may be unbounded.

In order to handle the various inequality literals in a more uniform way, we introduce new binary relation symbols < k (for k ∈ N) that are defined by a < k b if and only if a < b + k. Observe that s < k t entails s < n t whenever k ≤ n. Obviously, we may replace every literal s < t by s < 0 t, every literal s ≤ t by s < 1 t, and every literal s < ζ + k by s < k ζ. Let N 1 be the resulting clause set.

We will now transform N 1 into an equivalent set N 2 of ground clauses. We start by eliminating all equality literals that contain variables by exhaustively applying the following transformation rules:

N ∪ { C ∨ ζ ≈ ζ } → N ∪ { C } N ∪ { C ∨ ζ ≈ t } → N ∪ { C[ζ → t] } if t = ζ N ∪ { C ∨ ζ ≈ ζ } → N N ∪ { C ∨ ζ ≈ t } → N ∪ { C ∨ ζ < 1 t, C ∨ t < 1 ζ } if t = ζ
All variables in inequality literals are then eliminated in a Fourier-Motzkin-like manner by exhaustively applying the transformation rule

N ∪ { C ∨ i∈I ζ < ki s i ∨ j∈J t j < nj ζ } → N ∪ { C ∨ i∈I j∈J t j < ki+nj s i }
where ζ does not occur in C and one of the index sets I and J may be empty.

The clauses in N 2 are constructed over the finite set T of proper ground terms, but the length of the clauses in N 2 is potentially unbounded. In the next step, we will transform the clauses in such a way that any pair of terms s, t from T is related by at most one literal in any clause: We apply one of the following transformation rules as long as two terms s and t occur in more than one literal:

N ∪ { C ∨ s < k t ∨ s ≈ t } → N ∪ { C ∨ s < k t } if k ≥ 1 N ∪ { C ∨ s < 0 t ∨ s ≈ t } → N ∪ { C ∨ s < 1 t } N ∪ { C ∨ s < k t ∨ s ≈ t } → N if k ≥ 1 N ∪ { C ∨ s < 0 t ∨ s ≈ t } → N ∪ { C ∨ s ≈ t } N ∪ { C ∨ s < k t ∨ s < n t } → N ∪ { C ∨ s < n t } if k ≤ n N ∪ { C ∨ s < k t ∨ t < n s } → N if k + n ≥ 1 N ∪ { C ∨ s < 0 t ∨ t < 0 s } → N ∪ { C ∨ s ≈ t } N ∪ { C ∨ L ∨ L } → N ∪ { C ∨ L } for any literal L N ∪ { C ∨ s ≈ t ∨ s ≈ t } → N
The length of the clauses in the resulting set N 3 is now bounded by 1 2 m(m + 1), where m is the cardinality of T . Still, due to the indices of the relation symbols < k , N 3 may be infinite. We introduce an equivalence relation ∼ on clauses in N 3 as follows: Define C ∼ C if for all s, t ∈ T (i) s ≈ t ∈ C if and only if s ≈ t ∈ C , (ii) s ≈ t ∈ C if and only if s ≈ t ∈ C , and (iii) s < k t ∈ C for some k if and only if s < n t ∈ C for some n. This relation splits N 3 into at most ( 1 2 m(m + 1)) 5 equivalence classes. 16We will now show that each equivalence class is logically equivalent to a finite subset of itself. Let M be some equivalence class. Since any two clauses from M differ at most in the indices of their < k -literals, we can write every clause

C i ∈ M in the form C i = C ∨ 1≤l≤n s l < k il t l
where C and the s l and t l are the same for all clauses in M . As we have mentioned above, s l < k il t l entails s l < k jl t l whenever k il ≤ k jl ; so a clause C i ∈ M entails C j ∈ M whenever the n-tuple (k i1 , . . . , k in ) is pointwise smaller or equal to the n-tuple (k j1 , . . . , k jn ) (that is, k il ≤ k jl for all 1 ≤ l ≤ n). Let Q be the set of n-tuples of natural numbers corresponding to the clauses in M . By Dickson's lemma [START_REF] Dickson | Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors[END_REF], for every set of tuples in N n the subset of minimal tuples (w. r. t. the pointwise extension of ≤ to tuples) is finite. Let Q be the subset of minimal tuples in Q, and let M be the set of clauses in M that correspond to the tuples in Q . Since for every tuple in Q \ Q there is a smaller tuple in Q , we know that every clause in M \ M is entailed by some clause in M . So the equivalence class M is logically equivalent to its finite subset M . Since the number of equivalence classes is also finite and all transformation rules are sound, this proves our claim.

In order to apply this theorem to hierarchic superposition, we must again impose some restrictions on the calculus. Most important, we have to change the definition of weak abstraction slightly: We drop the requirement that target terms are not domain elements from Def. 5.1, i. e., we abstract out a non-variable BG term q occurring in a clause C[f (s 1 , . . . , q, . . . , s n )], where f is a FG operator or at least one of the s i is a FG or impure BG term, even if q is a domain element. As we mentioned, all results obtained so far hold also for the modified definition of weak abstraction. In addition, we must again restrict to suitable Simp inferences (Def. 10.3). With these restrictions, we can prove our main result: Theorem 11.2. The hierarchic superposition calculus is dynamically refutationally complete w. r. t. LIA over Z for finite sets of Σ-clauses in which every proper BG-sorted term is either (i) ground, or (ii) a variable, or (iii) a sum ζ + k of a variable ζ and a number k ≥ 0 that occurs on the right-hand side of a positive literal s < ζ + k.

Proof. Let N be a finite set of Σ-clauses with the required properties. By Lemma 9.8, a pre-derivation starting from N 0 = abstr(N ) yields a locally sufficiently complete finite set N 0 of abstracted clauses. Now we run the hierarchic superposition calculus on N 0 (with the same restrictions on simplifications as in Sect. 10). Let N 1 be the (possibly infinite) set of BG clauses generated during the run. By unabstracting these clauses, we obtain an equivalent set N 2 of clauses that satisfy the conditions of Thm. 11.1, so N 2 is satisfiable in LIA over Z if and only if N is satisfiable w. r. t. the firstorder theory of LIA. Since the hierarchic superposition calculus is dynamically refutationally complete w. r. t. the first-order theory of LIA, the result follows.

Analogous results hold for linear rational arithmetic. Let n be the least common divisor of all numerical constants in the original clause set; then we define a < 2i b by a < b + i n and a < 2i+1 b by a ≤ b + i n for i ∈ N and express every inequation literal in terms of < k . The Fourier-Motzkin transformation rule is replaced by

N ∪ { C ∨ i∈I ζ < ki s i ∨ j∈J t j < nj ζ } → N ∪ { C ∨ i∈I j∈J t j < ki•nj s i }
where ζ does not occur in C, one of the index sets I and J may be empty, and k • n is defined as k + n -1 if both k and n are odd, and k + n otherwise. The rest of the proof proceeds in the same way as before.

Experiments

We implemented the HSP calculus in the theorem prover Beagle. 17 Beagle is a testbed for rapidly trying out theoretical ideas but it is not a high-performance prover (in particular it lacks indexing of any form). The perhaps most significant calculus feature not yet implemented is the improvement for linear integer and rational arithmetic of Sect. 11.

Beagle's proof procedure and background reasoning, in particular for linear integer arithmetic, and experimental results have been described in [START_REF] Baumgartner | Beagle -A Hierarchic Superposition Theorem Prover[END_REF]. Here we only provide an update on the experiments and report on complementary aspects not discussed in [START_REF] Baumgartner | Beagle -A Hierarchic Superposition Theorem Prover[END_REF]. More specifically, our new experiments are based on a more recent version of the TPTP problem library [START_REF] Sutcliffe | The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0[END_REF] (by four years), and we discuss in more detail the impact of the various calculus variants introduced in this paper. We also compare Beagle's performance to that of other provers.

We tested Beagle on the first-order problems from the TPTP library, version 7.2.0,18 that involve some form of arithmetic, including non-linear, rational and real arithmetics. The problems in the TPTP are organized in categories, and the results for some of them are quickly dealt with: none of the HWV-problems in the TPTP library was solvable within the time limit and we ignore these below. We ignore also the SYN category as its sole problem is merely a syntax test, and the GEG category as all problems are zero-rated and easily solved by Beagle.

The experiments were run on a MacBook Pro with a 2.3 GHz Intel i7 processor and 16 GB main memory. The CPU time limit was 120 seconds (a higher time limit does not help much solving more problems). Tables 1 and2 summarize the results for the problems with a known "theorem" or "unsatisfiable" status with non-zero rating. Beagle can also solve some satisfiable problems, but most of them are rather easy and can be solved by the BG solver alone. Unfortunately, the TPTP does not contain reasonably difficult satisfiable problems from the GBT-fragment, which would be interesting for exploiting the completeness result of Sect. 10.

Table 1 is a breakdown of Beagle's performance by TPTP problem categories and four flag settings. Beagle features a host of flags for controlling its search, but in Table 1 we varied only the two most influential ones: one that controls whether input arithmetic variables are taken as ordinary variables or as abstraction variables. (Sect. 5 discusses the trade-off between these two kinds of variables.) The other controls whether simplification of BG terms is done cautiously or aggressively.

To explain, the cautious simplification rules comprise evaluation of arithmetic terms, e. g. 3 • 5, 3 < 5, α + 1 < α + 1 (equal lhs and rhs terms in inequations), and rules for TPTP-operators, e. g., to_rat(5), is_int (3.5). For aggressive simplification, integer sorted subterms are brought into a polynomial-like form and are evaluated as much as possible. For example, the term 5 • α + f(3 + 6, α • 4) -α • 3 becomes 2 • α + f(9, 4 • α). These conversions exploit the associativity and commutativity laws for + and •. We refer the reader to [START_REF] Baumgartner | Beagle -A Hierarchic Superposition Theorem Prover[END_REF] for additional aggressive simplification rules, but we note here that aggressive simplification does not always preserve sufficient completeness. For example, in the clause set N = {P(1 + (2 + f(X))), ¬P(1 + (X + f(X)))} the first clause is aggressively simplified, giving N = {P(3 + f(X)), ¬P(1 + (X + f(X)))}. Both N and N are LIA-Table 1. Number of TPTP version 7.2.0 problems solved, of all non-zero rated "theorem" or "unsatisfiable" problems involving any form of arithmetic. The flag settings giving the best result are in typeset in bold. The CPU time limit was 120 seconds. The column "Any" is the number of problems solved in the union of the four setting to its left. For the "Auto" column see the description of auto-mode in the main text further below. For auto-mode only, the CPU time limit was increased to 300 seconds. unsatisfiable, sgi(N ) ∪ GndTh(LIA) is unsatisfiable, but sgi(N ) ∪ GndTh(LIA) is satisfiable. Thus, N is (trivially) sufficiently complete while N is not. These two flag settings, in four combinations in total, span a range from "most complete but larger search space" by using ordinary variables and cautious simplification, to "most incomplete but smaller search space" by using abstraction variables and aggressive simplification. As the results in Table 1 show, the flag setting "abstraction variables" solves more problems than "ordinary variables", but not uniformly so. Indeed, as indicated by the "Any" column in Table 1, there are problems that are solved only with either ordinary or abstraction variables. Some more specific comments, by problem categories:

Ordinary variables

ARI Of the 362 solved problems, 14 are not solved in every setting. Of these, four problems require cautious simplification, and five problems require aggressive simplification. This is independent from whether abstraction or ordinary variables are used.

DAT The DAT category benefits significantly from using ordinary variables.

There is only one problem, DAT075=1.p, that is not solved with ordinary variables. Two problems, DAT072=1.p and DAT086=1.p are solvable only with ordinary variables and aggressive simplification. Many problems in the DAT category, including DAT086=1.p, state existentially quantified theorems about data structures such as arrays and lists. If they are of an arithmetic sort, these existentially quantified variables must be taken as ordinary variables. This way, they can be unified with BG-sorted FG terms such as head(cons(x, y)) (which appear in the list axioms) which might be necessary for getting a refutation at all.

A trivial example for this phenomenon is the entailment {P(f(1))} |= ∃x P(x), where f is BG-sorted, which is provable only with ordinary variables.

NUM This category requires abstraction variables. With it, four of the problems can be solved in the NUM category (NUM859=1.p, NUM860=1.p, NUM861=1.p, NUM862=1.p), as the search space with ordinary variables is too big.

SWW By and large, cautious BG simplification fares slightly better on the SWW problems. Of the 97 problems solved, 16 are not solved in every setting, and the settings that do solve it do not follow an obvious pattern.

We were also interested in Beagle's performance, on the same problems, broken down by the calculus features introduced in this paper. Table 2 summarizes our findings for five configurations x-| obtained by progressively enabling these features. In order to assess the usefulness of the features we filtered the results by problem rating. The column "≥ 0.75", for instance, lists the number of solved problems, of all 80 known "theorem" or "unsatisfiable" problems with a rating 0.75 or higher and that involve some form of arithmetic. The predecessor calculus of [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] uses an exhaustive abstraction mechanism that turns every side of an equation into either a pure BG or pure FG term. All BG variables are always abstraction variables. Configuration x implements this calculus, with the only deviation of an added splitting rule. The splitting rule [START_REF] Weidenbach | SPASS version 3.5[END_REF] breaks apart a clause into variable-disjoint parts and leads to a branching search space for finding corresponding sub-proofs. See again [START_REF] Baumgartner | Beagle -A Hierarchic Superposition Theorem Prover[END_REF] for more details.

In our experiments splitting is always enabled, in particular also for configuration x for better comparability of result. Cautious BG simplification is enabled for configuration x and the subsequent configurations y-{. the ceiling or floor function, which is currently not implemented, and hence cannot be attempted.

In general, many problems used in the competition are rather large in size or search space and would require a more sophisticated implementation of Beagle.

Conclusions

The main theoretical contribution of this paper is an improved variant of the hierarchic superposition calculus. One improvement over its predecessor [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] is a different form of "abstracted" clauses, the clauses the calculus works with internally. Because of that, a modified completeness proof is required. We have argued informally for the benefits over the old calculus in [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF]. They concern making the calculus "more complete" in practice. It is hard to quantify that exactly in a general way, as completeness is impossible to achieve in presence of background-sorted foreground function symbols (e. g., "head" of integer-sorted lists). To compensate for that to some degree, we have reported on initial experiments with a prototypical implementation on the TPTP problem library. These experiments clearly indicate the benefits of our concepts, in particular the definition rule and the use of ordinary variables. There is no problem that is solved only by the old calculus only. Certainly more experimentation and an improved implementation is needed to also solve bigger-sized problems with a larger combinatorial search space.

We have also obtained two new completeness results for certain clause logic fragments that do not require compactness of the background specification, cf. Sect. 10 and Sect. 11. The former is loosely related to the decidability results in [START_REF] Kruglov | Superposition decides the first-order logic fragment over ground theories[END_REF], as discussed in Sect. 9. It is also loosely related to results in SMTbased theorem proving. For instance, the method in [START_REF] Ge | Complete instantiation for quantified formulas in satisfiabiliby modulo theories[END_REF] deals with the case that variables appear only as arguments of, in our words, foreground operators. It works by ground-instantiating all variables in order to being able to use an SMTsolver for the quantifier-free fragment. Under certain conditions, finite ground instantiation is possible and the method is complete, otherwise it is complete only modulo compactness of the background theory (as expected). Treating different fragments, the theoretical results are mutually non-subsuming with ours. Yet, on the fragment they consider we could adopt their technique of finite ground instantiation before applying Thm. 10.7 (when it applies). However, according to

  is a model of N by I |= N ; I |= C is short for I |= {C}. We say that N entails N , and write N |= N , if every model of N is a model of N ; N |= C is short for N |= {C}. We say that N and N are equivalent, if N |= N and N |= N .

  [ζ → qτ ] and τ = τ [ζ → qτ ] are again simple substitutions and Dτ is a simple ground instance of D. This implies that I is a model of Dτ . The clause Dτ has the form Dτ = Cτ [ζτ ] ∨ ζτ ≈ qτ ; since ζτ = qτ , Cτ = Cτ and qτ = qτ , this is equal to Cτ [qτ ] ∨ qτ ≈ qτ . Obviously, the literal qτ ≈ qτ must be false in I, so I must be a model of Cτ [qτ ] = C[q]τ = Cτ .

Theorem 6 . 1 .

 61 The inference rules of HSP Base are sound w. r. t. |= B , i. e., for every inference with premises in N and conclusion C, we have N |= B C. Proof. Equality resolution, Negative superposition, Positive superposition, and Equality factoring are clearly sound w. r. t. |=, and therefore also sound w. r. t. |= B . For Close, soundness w. r. t. |= B follows immediately from the definition.

Corollary 7 . 6 .

 76 Let I ∈ B be a term-generated Σ B -interpretation. Then E I ∪ D I |= GndTh(B). Proof. Since I ∈ B, we have I |= GndTh(B), hence E I ∪ D I |= GndTh(B) by Lemma 7.5. Let N be a set of weakly abstracted clauses and I ∈ B be a term-generated Σ B -interpretation, then N I denotes the set E I ∪ D I ∪ { Cσ | σ simple, reduced with respect to E I , C ∈ N , Cσ ground }. Lemma 7.7. If N is a set of weakly abstracted clauses, then R S Inf (sgi(N ) ∪ GndTh(B)) ⊆ R S Inf (N I ). Proof. By part (i) of Thm. 6.3 we have obviously R S Inf (sgi(N )) ⊆ R S Inf (E I ∪ D I ∪ sgi(N ) ∪ GndTh(B)). Let C be a clause in E I ∪ D I ∪ sgi(N ) ∪ GndTh(B) and not in N I . If C ∈ GndTh(B), then it is true in I, so by Lemma 7.5 it is either contained in E I ∪ D I ⊆ N I or it follows from smaller clauses in E I ∪ D I and is therefore in R S Cl (E I ∪ D I ∪ sgi(N )). If C / ∈ GndTh(B), then C = C σ for some C ∈ N , so it follows from C ρ and E I ∪ D I , where ρ is the substitution that maps every variable ζ to the E I -normal form of ζσ. Since C follows from smaller clauses in

  is needed for soundness, and condition (iii) is needed for completeness. The Simp rule covers the usual simplification rules of the standard superposition calculus, such as demodulation by unit clauses and deletion of tautologies and (properly) subsumed clauses. It also covers simplification of arithmetic terms, e. g., replacing a subterm (2 + 3) + α by 5 + α and deleting an unsatisfiable BG literal 5 + α < 4 + α from a clause. Any clause of the form C ∨ ζ ≈ d where d is domain element can be simplified to C[ζ → d].

Corollary 8 . 7 .

 87 Let J be a Σ-interpretation and I = nojunk(J). Let Cσ by a ground instance of a clause C. Then there is a smooth ground instance Cτ of C such that (tσ) I = (tτ ) I for every term occurring in C and such that I |= Cσ if and only if I |= Cτ . Proof. Using the previous lemma, we define τ such that for every variable ζ occurring in C, (ζτ ) I = (ζσ) I and all BG-sorted (proper or non-proper) subterms of ζτ are BG terms. Clearly τ is smooth. The other properties follow immediately by induction over the term or clause structure. Lemma 8.8. Let N be a set of Σ-clauses that is locally sufficiently complete. Let I ∈ B be a Σ B -interpretation, let J be a Σ-model of sgi(N ) ∪ E I ∪ D I , and let J = nojunk(J). Let C ∈ N and let Cτ by a smooth ground instance in smgi(N ) \ R S Cl (smgi(N ) ∪ E I ∪ D I ). Then (tτ ) J = (tτ ) J for every term t occurring in C and J |= Cτ if and only if J |= Cτ .

  First we observe that by Lemma 8.5 J |= E I ∪ D I . Using the result of the first step, this implies that J is a model of (smgi(N ) \ R S Cl (smgi(N ) ∪ E I ∪ D I )) ∪ E I ∪ D I , and since this set is a superset of (smgi(N ) ∪ E I ∪ D I )\R S Cl (smgi(N ) ∪ E I ∪ D I ), J is also a model of the latter. By Def. 6.2-(i), (smgi(N )

Theorem 9 . 2 .

 92 The inference rules of HSP are satisfiability-preserving w. r. t. |= B , i. e., for every inference with premise N and conclusion N we have N |= B if and only if N |= B . Moreover, N |= B N .

Example 9 . 4 .

 94 The following clause set demonstrates the need for condition (v) in Define. Let N = {f(c) ≈ 1} and suppose condition (v) is absent. Then we obtain N = {f(c) ≈ α f(c) , α f(c) ≈ 1}. By demodulating the first clause with the second clause we get N = {f(c) ≈ 1, α f(c) ≈ 1}. Now we can continue with N as with N . The problem is, of course, that the new definition f(c) ≈ α f(c) is greater w. r. t. the term ordering than the parent clause, in violation of condition (v).

Lemma 10 . 5 .

 105 Let C 1 , . . . , C n be clean clauses. Assume a HSP Base inference with premises C 1 , . . . , C n and conclusion C. Then C is clean and every BG term occurring in unabstr(C) also occurs in some clause unabstr(C 1 ),. . . , unabstr(C n ).

Lemma 10 . 6 .

 106 Let N ∪ {C} be a set of clean clauses. If N ∪ {D} is obtained from N ∪ {C} by a suitable Simp inference then D is clean. Proof. Suppose N ∪ {D} is obtained from N ∪ {C} by a suitable Simp inference. We need to show properties (i)-(iii) of cleanness for D. That every BG term in D is pure follows from Def. 10.3-(iii). That every BG term in unabstr(D) is ground follows from Def. 10.3-(iv) and cleanness of C. Finally, property (iii) follows from Def. 10.3-(ii).

  s has a FG sort, let s 1 , . . . , s n be the maximal BG-sorted subterms of s = s[s 1 , . . . , s n ]. Since for every s i there is a ground BG term t i with s I i = t I i , we obtain s I = (s[s 1 , . . . , s n ]) I = (s[t 1 , . . . , t n ]) I . Set t := s[t 1 , . . . , t n ].

  Definition 9.1 (Unabstracted clause). A clause is unabstracted if it does not contain any disequation ζ ≈ t between a variable ζ and a term t unless t = ζ and ζ ∈ vars(t). Any clause can be unabstracted by repeatedly replacing C ∨ ζ ≈ t by C[ζ → t] whenever t = ζ or ζ / ∈ vars(t). Let unabstr(C) denote an unabstracted version of C obtained this way. If t = t[ζ 1 , . . . , ζ n ] is a term in C and ζ i is finally instantiated to t i , we denote its unabstracted version t[t 1 , . . . , t n ] by unabstr(t[ζ 1 , . . . , ζ n ], C). For a clause set N let unabstr

  ζ n ] is a minimal BG-sorted non-variable term with a toplevel FG operator, (ii) t[t 1 , . . . , t n ] = unabstr({t[ζ 1 , . . . , ζ n ], L[t[ζ 1 , . . . , ζ n ]] ∨ D}), (iii) t[t 1 , . . . , t n ] is ground, (iv) α t[t1,...,tn] is a parameter, uniquely determined by t[t 1 , . . . , t n ], and (v) L[t[ζ 1 , . . . , ζ n ]]∨D ∈ R H

Cl (N ∪ abstr({t[t 1 , . . . , t n ] ≈ α t[t1,...,tn] , L[α t[t1,...,tn] ]∨ D})).

Table 2 .

 2 Number of "theorem" or "unsatisfiable" problems solved, by calculus features and problem rating, excluding the HWV-problems.

					Rating, # Problems
				≥ 0.1	≥ 0.5	≥ 0.75	≥ 0.88
		Abstraction	Feature	756	187	80	55
	x	Standard	N/A	355	30	5	1
	y		+ Define	493	38	5	1
	z	Weak	+ Define	490	40	5	1
			+ Define
	{		+ Ordinary vars	500	44	5	1
			+ Define
			+ Ordinary vars
	|		+ BG simp aggressive	511	45	5	1

Table 3 .

 3 CADE ATP system competition results 2018 and Beagle's performance on the same problem sets.

		Vampire	Vampire	CVC4	Princess	Beagle
		4.3	4.1	1.6pre	170717	0.9.51
	#Solved TFI (of 125)	93	98	85	62	36
	#Solved TFE (of 75)	70	64	72	43	44
	#Solved TFA (of 200)	163	162	157	105	70

Without loss of generality we assume that there exists a distinct sort for every predicate.

This restriction to term-generated interpretations as models is possible since we are only concerned with refutational theorem proving, i. e., with the derivation of a contradiction.

To satisfy the technical requirement that all interpretations in B are term-generated, we assume that in this case ΣB is suitably extended by an infinite set of constants (or by one constant and one unary function symbol) that are not used in any input formula or theory axiom.

If Σ = ΣB, this definition coincides with the definition of satisfiability w. r. t. a class of interpretations that was given in Sect. 2. A set N of BG clauses is B-satisfiable if and only if some interpretation of B is a model of N .

In contrast to[START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF], we include GndTh(B) in the definition of sufficient completeness. (This is independent of the abstraction method; it would also have been useful in[START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF].)

Note that J need not be a B-interpretation.

As in[START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF], it is possible to strengthen the maximality condition by requiring that there exists some simple ground substitution ψ such that (s ≈ t)σψ is maximal in (s ≈ t ∨ C)σψ (and analogously for the other inference rules).

In contrast to[START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF], we include GndTh(B) in the redundancy criterion. (This is independent of the abstraction method used; it would also have been useful in[START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF].)

Typically, EI contains two kinds of clauses, namely clauses that evaluate nonconstant BG terms, such as 2 + 3 ≈ 5, and clauses that map parameters to domain elements, such as α ≈ 4.

In[START_REF] Kruglov | Superposition Modulo Theory[END_REF], it is required that every ground term that contains a (proper or improper) BG-sorted FG subterm must be larger than any (BG or FG) ground term that does not contain such a subterm.

Condition (i) of Simp is obviously satisfied and condition (iii) there is condition (v) of Define. Instead of condition (ii), Define inferences are only B-satisfiability preserving, which however does not endanger soundness.

A KBO with appropriate weights can be used for fin .

Any pair of terms s, t is related in all clauses of an equivalence class by either a literal s ≈ t, or s ≈ t, or s <n t for some n, or t <n s for some n, or no literal at all, so there are five possibilities per unordered pair of terms.

Beagle is available at https://bitbucket.org/peba123/beagle. The distribution includes the (Scala) source code and a ready-to-run Java jar-file.

http://tptp.org

Configuration y differs from configuration x only by an additional Define rule. (As said earlier, the Define rule can be added without problems to the previous calculus.) By comparing the results for x and y it becomes obvious that adding Define improves performance dramatically. This applies to the new calculus as well. The Define rule stands out and should always be enabled.

Configuration z replaces the standard abstraction mechanism of [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] by the new weak abstraction mechanism of Sect. 5. Weak abstraction seems more effective than standard abstraction for problems with a higher rating, but the data set supporting this conclusion is very small.

There are five problems, all from the SWW category 19 that re solved only with configuration y, and there is one problem, SWW607=2.p, that is solved only by configurations x and y.

There are four solvable problems with rating 0.75. These are ARI595=1.p -ARI598=1.p, which are "simple" problems involving a free predicate symbols over the integer background theory. The problem ARI595=1.p, for instance, is to prove the validity of the formula 20 The calculus and implementation techniques needed for solving such problems are rather different to those needed for solving combinatory problems involving trivial arithmetics only, like, e.g., the HWV-problems.

Configuration { is the same as z except that it includes the results for general variables instead of abstraction variables. Similarly, configuration | is the same as { except that it includes the results for aggressive BG simplification. It is the union of all results in Table 1.

For comparison with other implemented theorem provers for first-order logic with arithmetics, we ran Beagle on the problem set used in the 2018 edition of the CADE ATP system competition (CASC-J9). 21 . The competing systems were CVC4 [START_REF] Barrett | CVC4[END_REF], Princess [START_REF] Rümmer | A constraint sequent calculus for first-order logic with linear integer arithmetic[END_REF], and two versions of Vampire [START_REF] Kovács | First-order theorem proving and Vampire[END_REF].

In the competition, the systems were given 200 problems from the TPTP problem library, 125 problems over the integers as the background theory (TFI category), and 75 over the reals (TFE category). The system that solves the most problems in the union of the TFI and TFE categories within a CPU time limit of 300 sec wins. We applied Beagle in an "auto" mode, which time-slices (at most) three parameter settings. These differ mainly in their use of abstraction variables or ordinary variables, and the addition of certain arithmetic lemmas.

The results are summarized in Table 3. We note that Beagle was run on different hardware but the same timeout of 300 seconds. The results are thus only indicative of Beagle's performance, but we do not expect significantly different result had it participated. In the TFI category, of the 36 problems solved, 5 require the use of ordinary variables. In the TFE category, 16 problems involve 19 SWW583=2.p, SWW594=2.p, SWW607=2.p, SWW626=2.p, SWW653=2.p and SWW657=2.p 20 At the time of this writing, there are only four provers (including Beagle) registered with the TPTP web infrastructure that can solve these problems. Hence the rating 0.75. 21 http://tptp.cs.miami.edu/~tptp/CASC/J9/ Thm. 10.7 our calculus needs instantiation of background-sorted variables only, this way keeping reasoning with foreground-sorted terms on the first-order level, as usual with superposition.