{'fraction_non_alphanumeric': 0.05292289765002913, 'fraction_numerical': 0.008209890711347305, 'mean_word_length': 3.725077166930842, 'pattern_counts': {'":': 0, '<': 39, '<?xml version=': 0, '>': 12, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 79, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Hierarchic Superposition Revisited

Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are ``reasonably complete'' even in the presence of free function symbols ranging into a background theory sort. The hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we demonstrate, not optimally. This paper aims to rectify the situation by introducing a novel form of clause abstraction, a core component in the hierarchic superposition calculus for transforming clauses into a form needed for internal operation. We argue for the benefits of the resulting calculus and provide two new completeness results: 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.


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 [23] for the quantifier-free case by instantiation heuristics for quantifiers [15, 16, e. g.].
Another line of research is concerned with adding black-box reasoners for specific background theories to first-order automated reasoning methods (resolution [5,17,1], sequent calculi [25], instantiation methods [14,8,9], 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 [5], 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 hierarchical superposition 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 by Bachmair, Ganzinger, and Waldmann, however, 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 instead of one, 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 (1). 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 [5] 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 [5] 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 [5] 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 [5]. 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 (1), 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 [26].
Sections 1-7, 9-10, and 12 of this paper are a substantially expanded and revised version of [11]. A preliminary version of Sect. 11 has appeared in [10].
Related Work. The relation with the predecessor calculus in [5] 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 [20] will be discussed in Sect. 9 below. The resolution calculus in [17] 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 [8,9] lacks the treatment of background-sorted foreground function symbols. The same applies to the sequent calculus in [25], which treats linear arithmetic with built-in rules for quantifier elimination. The instantiation method in [14] 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 [21,2,12]. 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 [21], 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 is a model of N by I |= N ; I |= C is short for I |= {C}. We say that N entails N ′ , and write N |= 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 derive 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. In this case, B is trivially compact; in fact, a set N of Σ B -clauses is B-unsatisfiable if and only if some clause of N is B-unsatisfiable. (2) Σ B is extended by an infinite number of parameters, that is, additional constant symbols. While all interpretations in B share the same carrier sets {I ξ } ξ∈ΞB and interpretations of non-parameter symbols, parameters may be interpreted freely by arbitrary elements of the appropriate I ξ . The class B obtained in this way is in general not compact; for instance the infinite set of clauses { n ≤ β | n ∈ N }, where β is a parameter, is unsatisfiable in the integers, but every finite subset is satisfiable. (3) Σ B is again extended by parameters, however, B is now the class of all 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 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. 6 Our 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, 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. 8 ⊓ ⊔ For 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. 6 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 . 7 In contrast to [5], we include GndTh(B) in the definition of sufficient completeness.
(This is independent of the abstraction method; it would also have been useful in [5].) 8 Note that J need not be a B-interpretation.

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 called

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 [5] 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 [5] 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 [5] 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 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 [5] 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 [5]. In fact, it was claimed in a footnote in [5] 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 [5] 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 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) + (α + 1), z) ≈ β yields g(1, X, f(1)+ Y, z) ≈ β ∨X ≈ α∨Y ≈ α+ 1. Note that the terms 1, f(1)+ (α+ 1), z, and β are not abstracted out: 1 is a domain element; f(1) + (α + 1) has a BG sort, but it is not a BG term; z is a variable; and β is not a proper subterm of any other term. The clause write(a, 2, read(a, 1) + 1) ≈ b is already weakly abstracted. Every pure BG clause is trivially weakly abstracted. 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.) It is easy to see that the abstraction process described in Def. 5.1 does in fact terminate. For any clause, we consider the multiset of the numbers of nonvariable occurrences in the left and right-hand sides of its literals: If we abstract out a target term q, then q has k ≥ 1 non-variable occurrences and it occurs as a subterm of a left or right-hand side s[q] with n > k non-variable occurrences. After the abstraction step, s[ζ] has n−k non-variable occurrences and the two terms ζ and q in the new abstraction literal have 0 and k non-variable occurrences. Since n−k, k, and 0 are strictly smaller than n, the multiset decreases. Termination follows from the well-foundedness of the multiset ordering.
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 [ζ → 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τ . 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: ¬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: 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. ⊓ ⊔ In the rest of the paper we will need some technical lemmas that relate clauses, their (partial) abstractions, instances of these clauses, and the target terms in these clauses.
If wσ is a target term in K, then w is a variable or a target term in L.
Proof. If w is neither a variable nor a target term in L, then w is a FG term or a domain element, or it equals v, or it occurs below a BG operator f and all other terms occurring below f are pure BG terms. Each of these properties is preserved by instantiation with a simple substitution. (Note that simple instances of pure BG terms are again pure BG terms.) ⊓ ⊔ Let σ be a substitution that maps all abstraction variables in its domain to pure BG terms and all ordinary BG-sorted variables in its domain to impure BG terms, and let Proof. The term w is a target term in L if and only if (i) w is a BG term that is neither a domain element nor a variable, and (ii) w occurs in L in a term f (s 1 , . . . , w, . . . , s n ), where f is a FG operator or at least one of the s i is a FG or impure BG term. Obviously wσ cannot be a domain element or a variable. Moreover it is easy to check that σ maps BG terms to BG terms, impure BG terms to impure BG terms, and FG terms to FG terms, so both properties (i) and (ii) are preserved by σ. ⊓ ⊔ Lemma 5.6. Let D 0 be a clause. Let τ 0 be a simple substitution such that D 0 τ 0 is a ground instance of D 0 and let ρ 0 be the identity substitution. For n ∈ {0, . . . , k−1} let D n+1 be clauses obtained from D 0 by successively abstracting out target terms as described in Def. 5.1, that is, let q n be a target term in D n = D n [q n ] and let D n+1 = D n [ζ n ] ∨ ζ n ≈ q n (where ζ n is a new abstraction variable, if q n is a pure target term, and a new ordinary variable otherwise). Let τ n+1 = τ n [ζ n → q n τ n ] and ρ n+1 = ρ n [ζ n → q n ρ n ]. Then the following properties hold: (1) If n ∈ {0, . . . , k}, then τ n and ρ n are simple substitutions and ρ n maps all abstraction variables in its domain to pure BG terms and all ordinary variables in its domain to impure BG terms. (2) If n ∈ {0, . . . , k}, then τ n = ρ n τ 0 .
(3) If n ∈ {0, . . . , k} then D n τ n is a ground instance of D n and has the form instances of the abstraction literals introduced so far. (4) If n ∈ {0, . . . , k} and if D ′ n is the subclause of D n that is obtained by dropping the abstraction literals introduced so far, then D ′ n ρ n = D 0 . (5) If n ∈ {0, . . . , k−1} and if the target term q n occurs in the subclause D ′ n of D n , then there is a target termq n in D 0 such that q n τ n =q n τ 0 .
Proof. Property (1) follows by induction from the fact that all the mappings [ζ n → q n τ n ] and [ζ n → q n ρ n ] are simple and from the fact that [ζ n → q n ρ n ] maps an abstraction variable to a pure BG term or an ordinary variable to an impure BG term.
Property (2) is obvious for n = 0. By induction, we obtain Property (3) is again obvious for n = 0. By induction, we obtain Since q n is a subterm of D n and D n τ n is ground by induction, we can conclude that q i τ n ≈ q i τ n is ground as well.
To prove property (4), we write D n in the form D n = D ′ n ∨ E n , where E n is the subclause consisting of all abstraction literals introduced so far. For . It remains to prove property (5). By property (4) ρ n maps D ′ n to D 0 ; since q n occurs in D ′ n , q n ρ n is a subtermq n of D 0 . By property (1) and Lemma 5.5, q n must be a target term in D 0 . Property (2) yieldsq n τ 0 = q n ρ n τ 0 = q n τ n . ⊓ ⊔

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 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
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)σ. 10 For example, Equality resolution is applicable to

and (viii) none of the premises has selected literals.
Equality factoring 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.
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.
Theorem 6.1. 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.
⊓ ⊔ 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 manysorted logics with subsorts [27]. As we will see below, such substitutions never need to be considered.
More precisely, we call a simple substitution for every abstraction variable X ∈ X B . That is, a restricted simple substitution maps every abstraction variable to an abstraction variable or a domain element.
Proposition 6.2. Let s and t be subterms of weakly abstracted clauses such that σ is a simple most general unifier of s and t and sσ is not a pure BG term. Then σ is a restricted substitution.
Proof. Since σ is a simple unifier of s and t, we have sσ = tσ. Moreover, simple substitutions map pure BG terms to pure BG terms, so we know that neither s nor t are pure BG terms. This leaves the following possibilities: Case 1: s or t is an ordinary BG variable x. In this case, σ has the form [x → t] or [x → s], and since Y σ = Y for every abstraction variable, this is obviously a restricted substitution. Case 2: s or t is a non-variable impure BG term. Without loss of generality assume that s is a non-variable impure BG term, and that, if t is also a nonvariable impure BG term, the depth of s is not smaller than the depth of t (otherwise swap s and t). The term s has the form f (s 1 , . . . , s k ), where f is a BG operator symbol. Since s occurs in a weakly abstracted clause, it may not contain any target terms, so we have either that every s i is a variable or a domain element and at least one s j is an ordinary variable, or that exactly one s j is a non-variable impure BG term and every s i , i = j, is an abstraction variable or a domain element. Let p be the position of the deepest operator symbol in s that is not a domain element. We apply the decomposition rule exhaustively to the unifiability problem {s . = t} and obtain a unifiability problem Clearly σ is also a most general unifier of M . Case 2.1: t| p = g(. . . ). Then u 1 , . . . , u k are direct subterms of s| p , so they are either BG variables or domain elements; u k+1 , . . . , u n are either BG abstraction variables or domain elements; and v 1 , . . . , v k are direct subterms of t| p . Case 2.1.1: t is also an impure BG term. Then v 1 , . . . , v k are also BG variables or domain elements, and v k+1 , . . . , v n are also BG abstraction variables or domain elements. Consequently, σ binds every variable to a variable or a domain element, so it is restricted.
Case 2.1.2: t is a FG term. Then (every subterm of) every v i must be a variable, or a domain element, or a FG term, otherwise it would be a target term. So σ cannot map an abstraction variable to a BG term that is neither a variable nor a domain element, hence it is again restricted. Case 2.2: t| qj = ζ for some proper prefix q of p. Then u 1 , . . . , u k are direct subterms of s| q , so u j is a non-variable impure BG term and every u i , i = j is a BG abstraction variable or a domain element; u k+1 , . . . , u n are either BG abstraction variables or domain elements; and v 1 , . . . , v k are direct subterms of t| q , where v j = ζ.
Case 2.2.1: v j = ζ is an abstraction variable X. Then every equation u i .
= v i contains at least one pure BG term, so sσ = tσ is a pure BG term, contradicting the assumption.
Since v i σ = u i σ for every i, each v i must be a BG term; since v j is an impure BG term this implies that every v i , i = j, must be a variable or domain element (otherwise it would be a target term). Assume that for some l = j, v l agrees with x.
In M ′ , however, every equation contains at least one pure BG term, so sσ = tσ would be a pure BG term, contradicting the assumption. Therefore we know that the variable x occurs only once in M . Consequently, σ maps every variable except x to a variable or a domain element; since x is an ordinary variable, this implies that σ is restricted.
Case 3: Both s and t are FG terms. Since s and t occur in weakly abstracted clauses, neither s nor t can contain a BG subterm that is not a variable or a domain element. Therefore σ cannot map any pure variable X to a BG term that is not a variable or a domain element, so σ is restricted.
⊓ ⊔ By condition (ii) in the Equality resolution inference rule, Prop. 6.2 guarantees that any simple mgu σ of an Equality resolution inference is restricted. The same holds true analogously for the other inference rules. As a consequence, unification algorithms do not need to compute weakening substitutions. In essence, a suitably modified standard unification algorithm needs to prevent binding an abstraction variable to a term other than an abstraction variable or a domain element.
For example, the (weakly abstracted) clause of s and t, the term sσ = (X + Y ) + U is pure BG, hence violating condition (ii) in Equality resolution, and so σ does not need to be computed in the first place.
In contrast to [5], 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 [5], 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 .) 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 ′ : 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 [3], Nieuwenhuis [22], Nieuwenhuis and Rubio [24]). To define a redundancy criterion for HSP Base and to prove the refutational completeness of the calculus, we use the same approach as in [5] 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 [3] and [22]: Theorem 6.4. 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.5. 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

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 [5]: 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 for both properties are similar to the corresponding ones in [5]; 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.
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 ≈ 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 ι.
from weakly abstracted premises with pivotal substitution σ. Let ι ′ be a simple ground instance of ι of the form In contrast to [5], we include GndTh(B) in the redundancy criterion. (This is independent of the abstraction method used; it would also have been useful in [5].) 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 ι ′ .
Proof. Without loss of generality, we may assume that σ is an idempotent most general unifier over vars(C 1 ) ∪ vars(C 2 ) and that τ = σρ for some substitution ρ; hence στ = σσρ = σρ = τ and in particular C 0 στ = C 0 τ . Let τ 0 = τ and let D 0 = C 0 σ. Let D n be the result of the nth abstraction step starting from D 0 for n ∈ {0, . . . , k}, and let abstr(C 0 σ) = D k . According to part (3) of Lemma 5.6, there are simple substitutions τ n for 1 ≤ n ≤ k such that D n τ n is a ground instance of D n and has the form where the literals q i τ i ≈ q i τ i are ground instances of the abstraction literals introduced so far and q i is a target term in D i . Since C 0 στ = D 0 τ = D 0 τ 0 , this clause has essentially the required form. We still have to prove, though, that each literal q i τ i ≈ q i τ i is smaller than the pivotal literal L of ι ′ .
If q i occurs in D i in a literal K that has been generated by the jth abstraction step (j < i), then Kτ j is a literal q j τ j ≈ q j τ j and q i τ i is a proper subterm of q j τ j . By induction on the number of abstraction steps we obtain If q i occurs in D i in a literal that has not been generated by a previous abstraction step, then by part (5) The termq i is either a term from C 1 σ, or a term from C 2 σ, or a subterm of the term s[r]σ (the last two cases are possible only for superposition inferences). We analyze these cases separately.
Case 1.1: C 1 does not have selected literals. In this case, every literal of C 1 τ is smaller than or equal to the pivotal literal L of ι ′ . Consequently, we obtain L. Case 1.2: C 1 has selected literals. In this case, L is a selected literal in C 1 τ and ι and ι ′ are either Negative superposition or Equality resolution inferences. Sincē q i is a target term in C 0 σ, it is not a variable.
Ifq i occurs in vσ below a variable position of v, then there is a ζ ∈ dom(σ) ∩ vars(C 1 ) such thatq i is a subterm of ζσ. Otherwise, there is a subterm w of v such thatq i = wσ. Since C 1 is weakly abstracted, w cannot be a target term, so by Lemma 5.4, w must be a variable ζ, and again ζ ∈ dom(σ) ∩ vars(C 1 ). So in both cases,q i is a subterm of ζσ, and consequently, q i τ i =q i τ is a subterm of ζστ = ζτ .
Let us first consider a Negative superposition inference operating on the literal As σ is a simple most general unifier of l and u and ζ ∈ dom(σ) ∩ vars(C 1 ), we know that ζ must occur in u. Moreover u is not a variable, so ζ is a proper subterm of u. This implies Otherwise ι is an Equality resolution inference operating on the literal s ≈ t in C 1 , where L = (s ≈ t)τ . As σ is a simple most general unifier of s and t and ζ ∈ dom(σ) ∩ vars(C 1 ), we know that ζ must occur in s or t. Assume without loss of generality that ζ occurs in s. If s = ζ, then by the restrictions on selection functions t must be a FG term, so ζτ = tτ is a FG term as well. Since the BG term q i τ i is a subterm of the FG term ζτ , it must be a proper subterm, hence q i τ i ≺ ζτ = tτ and q i τ i ≈ q i τ i ≺ (s ≈ t)τ = L. Otherwise ζ is a proper subterm of s, then q i τ i ζτ ≺ sτ = tτ and we obtain again This case is proved similarly to case 1.1 above: By the structure of SSP inferences, the literal lτ ≈ rτ of C 2 τ that has been used to replace sτ [lτ ] by sτ [rτ ] in the pivotal literal is strictly maximal in C 2 τ and lτ ≻ rτ . Consequently, we obtain q i τ i =q i τ ≺ vστ = vτ lτ sτ [lτ ] and thus Case 3: It remains to consider the case thatq i is a subterm of the term s[r]σ produced in a superposition inference. Then ). Using these two results we can prove the following lemmas: . Condition (iii) is obviously satisfied for all Close inferences. Suppose that ι is not a Close inference and its conclusion concl(ι) = abstr(C 0 ) is in N . Showing that ι ∈ R H Inf (N ) amounts to proving that every simple ground instance of ι is redundant w. r. t. sgi(N ) ∪ GndTh(B). Let ι ′ be such a simple ground instance with maximal premise C 1 τ and conclusion C 0 τ . By Lemma 7.2, 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 ι ′ .
By the structure of superposition inferences, the clause C 0 τ is obtained from C 1 τ by replacing the pivotal literal in C 1 τ by (zero or more) smaller literals. Since the literals in E are also smaller than the pivotal literal, C 0 τ ∨ E is still smaller than C 1 τ . Moreover, C 0 τ ∨ E entails C 0 τ , so ι ′ ∈ R S Inf (sgi(N ) ∪ GndTh(B)). As sgi(ι) ⊆ R S Inf (sgi(N ) ∪ GndTh(B)), the inference ι is contained in R H Inf (N ). This proves condition (iii).
We come now to the proof of condition (iv). Note that

⊓ ⊔
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 ′ Obviously, E ′ I is terminating, right-reduced, and 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}. It is fairly easy to prove that 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.

⊓ ⊔
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 }.
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 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 redundant with respect to N I , i. e., that it 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. 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 [5] 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.
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 [4]; 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: . Condition (ii) 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 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.
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.
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 [20] (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 [19]: 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 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 g(f(γ)) ≈ a ∨ g(f(β)) ≈ a  (6) and (7), and both are smaller than (8). 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 (8). 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 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 [19] 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: 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.
Lemma 8.5. Let J, J ′ , and nojunk(J) = J ′′ be given as above. Then the following properties hold: (v) If t is a ground term such that all BG-sorted subterms of t are BG terms, Proof. Properties (i)-(iv) follow directly from the definition of J ′ and J ′′ ; property (v) follows from (iv) by induction. 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 . 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 .
Since 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 ) 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 ) We can now show the main result of the lemma: We know that J ′′ is a termgenerated Σ-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τ of C such that J ′′ |= Cσ if and only if J ′′ |= Cτ . As the latter has been shown in the second step, the result follows. 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.
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).
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. 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 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.

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.
⊓ ⊔ 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. 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.
Lemma 10.5. Let C 1 , . . . , C n be clean clauses. Assume a HSP Base inference with premises C 1 , . . . , C n and conclusion C. Then the following holds: (1) C is clean.
Proof. Let C ′ be the conclusion of the inference before weak abstraction, i.e., C = abstr(C ′ ). Regarding (1), property (i) of cleanness for C, we are given that all BG terms in all premise clauses are pure. Unification does not introduce general variables, and hence every BG term in C ′ is pure. Weak abstraction never introduces ordinary variables unless the given clause has ordinary variables. Thus all BG terms in C are pure as well.
The remaining properties (ii) and (iii) of cleanness of C and property (2) can be seen from inspection of the HSP Base inference rules. We show it for superposition inferences, the other rules are similar. We distinguish three cases.
Case 1: the inference is a superposition inference into a subterm u of s i of a literal s ≈ t of the right premise, where s = f(s 1 , . . . , s i [u], . . . , s n ) and f is a BG-sorted foreground operator. With properties (i) and (iii) of cleanness holding for the premise clauses it follows that u must be FG-sorted. In the conclusion of the inference u is replaced by a FG-sorted term rσ where σ is the pivotal substitution. By Prop. 6.2 the substitution σ is restricted. This means that for every BG variable X occurring in C 1 or C 2 , if Xσ = X then Xσ is an (abstraction) variable occurring in C 1 or in C 2 , or Xσ is a domain element. Because neither variables nor domain elements are abstracted out, it follows that C ′ does not require further abstraction, i.e., C = C ′ .
By item (ii) of cleanness, every BG term in unabstr(C 1 ) and in unabstr(C 2 ) is ground. In other words, every BG variable occurring in C 1 or C 2 is replaced by a ground term by unabstraction. This holds in particular for Xσ if Xσ is a variable, as opposed to a domain element. It follows that every BG term in unabstr(C ′ ) = unabstr(C) is ground and that every BG term in unabstr(C) also occurs in unabstr(C 1 ) or unabstr(C 2 ), i.e., property (2) of the lemma claim. Finally observe that property (iii) of cleanness holds trivially for C, which completes the proof of property (1).
Case 2: the inference is a superposition inference into any other FG-sorted subterm. This is proved in essentially the same way as in case 1.
Case 3: the inference is a superposition inference into the top position of the left side of f(s 1 , . . . s n ) ≈ t, where f is a BG-sorted foreground operator. From item (iii) of cleanness it follows this term is replaced by a ground BG term t ′ , which does not need abstraction. The remaining argumentation is analogous to case 1 and is omitted. ⊓ ⊔ 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 [5] with a correspondingly modified Define rule and get Thm. 10.7 in that context as well.
Kruglov and Weidenbach [20] 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 [20] 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: All variables in inequality literals are then eliminated in a Fourier-Motzkin-like manner by exhaustively applying the transformation rule 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: 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. 16 We 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 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 [13], 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 already in Sect. 5, 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 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 [7]. Here we only provide an update on the experiments and report on complementary aspects not discussed in [7]. More specifically, our new experiments are based on a more recent version of the TPTP problem library [26] (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 and 2 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 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. becomes 2 · α + f(9, 4 · α). These conversions exploit the associativity and commutativity laws for + and ·. We refer the reader to [7] 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 LIAunsatisfiable, 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: 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 vari-ables. 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 ①-⑤ 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 [5] 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 ① implements this calculus, with the only deviation of an added splitting rule. The splitting rule [28] breaks apart a clause into variable-disjoint parts and leads to a branching search space for finding corresponding sub-proofs. See again [7] for more details.
In our experiments splitting is always enabled, in particular also for configuration ① for better comparability of result. Cautious BG simplification is enabled for configuration ① and the subsequent configurations ②-④.
Configuration ② differs from configuration ① 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 ① and ② 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 ③ replaces the standard abstraction mechanism of [5] 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 ②, and there is one problem, SWW607=2.p, that is solved only by configurations ① and ②.
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 (∀ z : Z a ≤ z ∧ z ≤ a + 2 → p(z)) → ∃ x : Z p(3 · x). 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 ③ 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 [6], Princess [25], and two versions of Vampire [18].
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 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/ 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 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 [5] 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 [5]. 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 [20], as discussed in Sect. 9. It is also loosely related to results in SMTbased theorem proving. For instance, the method in [16] 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 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.