Vincent Aravantinos
email: vincent.aravantinos@imag.fr

Nicolas Peltier
email: nicolas.peltier@imag.fr

A resolution calculus for first-order schemata *

Keywords: Propositional logic, first-order logic, schemata, resolution calculus

We devise a resolution calculus that tests the satisfiability of infinite families of clause sets, called clause set schemata. For schemata of propositional clause sets, we prove that this calculus is sound, refutationally complete, and terminating. The calculus is extended to first-order clauses, for which termination is lost, since the satisfiability problem is not semi-decidable for nonpropositional schemata. The expressive power of the considered logic is strictly greater than the one considered in our previous work.

Introduction

Many problems in mathematics or in formal verification can be specified as schemata of formulae, corresponding to infinite sequences of structurally similar formulae in some base language (e.g. propositional logic). Such schemata are parameterized by a natural number n and are usually defined by induction on n; in fact, the signature itself may depend on n. A typical example is the family of formulae:

p 0 ∧ n i=0 (p i ⇒ p i+1 ) ∧ ¬p n+1
and this schema is obviously unsatisfiable for all values of n ∈ N. Another example is:

(p ⇔ (¬p ⇔ (• • • (¬p ⇔ (p ⇔ (• • • )) • • • ))))
which formally corresponds to the following formula φ n defined by induction:

φ 0 ≡ true φ n+1 ≡ p ⇔ (¬p ⇔ φ n )
It is straightforward to verify that φ n is equivalent to true if n is even and to false if n is odd.

Examples of applications include the formal verification of inductively-defined hardware [START_REF] Gupta | Parametric Circuit Representation Using Inductive Boolean Functions[END_REF], since parameterized circuits can be easily described by schemata of propositional formulae. Another application is the automated verification of code fragments containing loops (the parameter then encodes the number of iterations). Similarly, some inductive proofs in mathematics may be modeled as schemata of proofs in first-order logic, the parameter being in this case the natural number on which the induction is based (see [START_REF] Baaz | CERES: An analysis of Fürstenberg's proof of the infinity of primes[END_REF] for an example of application of this technique). In such cases, schemata can be more natural and readable than an explicit induction, even though the underlying mechanism is still an induction. This is especially important in work like [START_REF] Baaz | CERES: An analysis of Fürstenberg's proof of the infinity of primes[END_REF] where the authors use the cut-elimination method CERES to analyze Furstenberg's topological proof of the infinity of primes. While existing SAT-solvers can be used to reason on any particular instance of these formulae, proving that a property holds for every value of the parameter obviously requires much more sophisticated reasoning techniques, using some form of mathematical induction and invariant generation.

Proof procedures already exist to test the validity of propositional schemata [START_REF] Aravantinos | Decidability and Undecidability Results for Propositional Schemata[END_REF]. The satisfiability problem, which consists in deciding whether there is a value of the parameter n for which the schema is satisfiable, is actually undecidable in general (it is obviously semi-decidable), but decision procedures can be defined for various subclasses, namely for regular [START_REF] Aravantinos | A Schemata Calculus For Propositional Logic[END_REF], regularly nested [START_REF] Aravantinos | A Decidable Class of Nested Iterated Schemata[END_REF] or bound-linear [START_REF] Aravantinos | Decidability and Undecidability Results for Propositional Schemata[END_REF] schemata. The present paper describes a new decision procedure, that is based on the resolution calculus [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF][START_REF] Leitsch | The resolution calculus[END_REF][START_REF] Bachmair | Resolution Theorem Proving[END_REF]. The proposed calculus is sound, refutationally complete and terminating. Its main advantage is that, unlike the procedure proposed in [START_REF] Aravantinos | A Schemata Calculus For Propositional Logic[END_REF] and [START_REF] Aravantinos | A Decidable Class of Nested Iterated Schemata[END_REF], its extension to first-order clauses is straightforward (see Section 8) although in this case termination and even refutational completeness can no longer be ensured. If restricted to propositional logic, the considered class of schemata is similar, but more general, than the class of regular schemata introduced in [START_REF] Aravantinos | A Schemata Calculus For Propositional Logic[END_REF]. It is not comparable to the other known decidable classes (note that regularly nested and bound-linear schemata may be transformed into regular ones at the cost of an exponential blow-up, see [START_REF] Aravantinos | Decidability and Undecidability Results for Propositional Schemata[END_REF] for details).

Families of (propositional) formulae may be expressed using a first-order syntax. For instance the first schema above can be denoted as follows:

∃n p 0 ∧ ∀i (i ≥ 0 ∧ i ≤ n ∧ p i ⇒ p s(i) ) ∧ ¬p s(n)
where the symbol s denotes the successor function. However, it should be noted that the formula is unsatisfiable only if n is interpreted as a natural number, and s as the standard successor function. The formula is clearly satisfiable on other domains (for instance one can take n = 1, s(0) = 0, s(1) = 1, p 0 = true, and p 1 = false). The usual resolution calculus therefore fails to prove the unsatisfiability of the previous schema. Testing the satisfiability of a formula in a fixed domain (such as N) is a very complex problem from a theoretical point of view. Due to well-known theoretical limitations, no refutationally complete proof procedure can possibly exist: the problem is not semi-decidable. Approaches designed to test the satisfiability in fixed domains include the integration of linear arithmetic into the superposition calculus [START_REF] Bachmair | Rewrite-based Equational Theorem Proving with Selection and Simplification[END_REF], which is considered in [START_REF] Waldmann | Superposition and Chaining for Totally Ordered Divisible Abelian Groups[END_REF][START_REF] Korovin | Integrating Linear Arithmetic into Superposition Calculus[END_REF][START_REF] Althaus | Superposition Modulo Linear Arithmetic SUP(LA)[END_REF] ( [START_REF] Bachmair | Refutational Theorem Proving for Hierachic First-Order Theories[END_REF] describes a general approach for hierarchic reasoning). In [START_REF] Horbach | Superposition for fixed domains[END_REF], a superposition-based calculus is proposed for reasoning on formulae in which the domain of interpretation of some constants (or existential variables) is fixed. These calculi are in some sense the starting point of our work. However, they are not complete in general, in the sense that no contradiction can be derived in finite time for some unsatisfiable clause sets (this is due to the fact that linear arithmetic is not compact), and they do not terminate on the class of problems that we consider. Note that completeness results exist for such calculi but they do not apply to our case.

We first show that propositional schemata can be encoded as sets of clauses in which some constant symbols (the parameters) denote natural numbers and must be interpreted as elements of N. The inductive rules defining the indexed formulae are also encoded as clauses. Then we define a resolution calculus operating on such sets of clauses. In this context, an application of the resolution rule can be interpreted either as a resolution inference in the usual sense or as an unfolding of an inductive definition. The resolution calculus does not terminate in general, even if the clause set is unsatisfiable (i.e. the calculus is not complete, although a very weak form of completeness can be stated). However we define a loop detection rule that is able to ensure both completeness and termination by automatically bounding the value of the parameter. This is done by generating so-called pruning clauses that are of the form n < k, where n is the parameter and k is a natural number. Once such a pruning clause is generated, the problem becomes essentially equivalent to a propositional one. In general, the pruning clauses are not logical consequences of the axioms, but they can be safely added into the clause set while retaining satisfiability.

The language we consider is of course weaker than those in [START_REF] Korovin | Integrating Linear Arithmetic into Superposition Calculus[END_REF][START_REF] Althaus | Superposition Modulo Linear Arithmetic SUP(LA)[END_REF][START_REF] Horbach | Superposition for fixed domains[END_REF] but on the other hand this approach ensures termination and refutational completeness for schemata of propositional clause sets. Although loop detection techniques and termination results already exist for the calculus in [START_REF] Horbach | Superposition for fixed domains[END_REF] (see also [START_REF] Horbach | Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries[END_REF]), strong restrictions are imposed on the syntax of the formulae (e.g. they must be Horn), which are not in general fulfilled by the formulae we consider in the present paper, even in the propositional case. Thus the techniques previously used to ensure termination are too weak for our purpose.

The rest of the paper is structured as follows. In Section 2, we define the syntax and semantics of the considered logic. In Section 3 we define the resolution calculus and establish a weak form of refutational completeness, then some additional syntactic restrictions are imposed on the clause sets in Section 4. In Section 5, we provide some hints on the expressive power of the obtained language and show how to encode schemata of propositional formulae. Sections 6 and 7 are the core of our work: in Section 6 a loop detection technique is presented and, in Section 7, the termination and refutational completeness of the resulting calculus is proved. Section 8 extends the calculus to first-order clauses (this is done as usual by lifting), although in this case refutational completeness does not hold (the satisfiability problem is not semi-decidable for schemata of first-order clause sets). Section 9 briefly concludes our work and identifies some lines of future research.

Preliminaries

For clarity and simplicity, we first restrict ourselves to schemata of propositional clause sets. The calculus will later be extended to first-order clauses (see Section 8). Informally, the syntax and semantics of our logic are almost identical to those of a very simple subclass of clausal logic, except that we consider a particular set of constant symbols, called parameters, that must be interpreted as natural numbers. Every predicate symbol is monadic and the only function symbols on the natural numbers are 0, s (s stands for the successor function).

Let Ω be a set of unary predicate symbols, or (indexed) propositional variables, and let P and V be two disjoint sets of variables. The elements in P are the parameters, and those in V are the index variables. Throughout this paper, parameters are denoted by n, m and index variables by x, y, z. The letters i, j, k, l will be used as meta-variables to represent natural numbers.

The set of (arithmetic) terms T is the least set satisfying V ⊆ T , 0 ∈ T and t ∈ T ⇒ s(t) ∈ T . Note that T does not contain any occurrence of a parameter. A term is ground if and only if it is of the form s i (0) (with i ∈ N), in which case it may be viewed as a natural number and simply denoted by i. The set of ground terms is denoted by N.

An atom is either of the form n ≈ t where n ∈ P and t ∈ T , or of the form p t where p ∈ Ω and t ∈ T ; the atom is ground if t is ground. Atoms of the form n ≈ t are called equational atoms and those of the form p t are called indexed atoms. Note that parameters only occur in equational atoms. A literal is either an atom (positive literal) or the negation of an atom (negative literal). A clause is a finite multiset (written as a disjunction) of literals and the empty clause is denoted by . An equational literal (resp. indexed literal) is a literal whose atom is an equational atom (resp. an indexed atom). We denote by C eq (resp. C idx ) the multiset of equational literals (resp. indexed literals) in C. If S is a set of clauses then S idx denotes the set of clauses {C idx | C ∈ S}. A clause C is purely equational if and only if C idx = ∅ and parameter-free if and only if C eq = ∅.

For every expression (term, atom, literal or clause) e, var(e) denotes the set of index variables occurring in e. The depth of an expression is defined as usual:

• depth(0) def = 0, depth(s(t)) def = 1 + depth(t), depth(x) def = 0 if x ∈ V; • depth(¬p t ) def = depth(p t ) def = depth(t), depth(n ≈ t) def = depth(n ≈ t) def = depth(t); • depth(l 1 ∨ . . . ∨ l k ) def = max i∈[1,k] depth(l i ), by convention depth( ) def = 0.
A substitution σ is a function mapping every index variable x to a term xσ ∈ T (in particular, a parameter cannot be substituted for and a variable cannot be mapped to a parameter either). The domain dom(σ) of σ is the set of index variables x such that xσ = x. For every expression e, eσ denotes the expression obtained from e by replacing every variable x by xσ. A substitution σ is ground if and only if for every x ∈ dom(σ), xσ is ground. A renaming is an injective substitution σ such that xσ ∈ V for every x ∈ dom(σ). A substitution σ is flat if for every x ∈ V, xσ ∈ V ∪ {0}. It is a unifier of t 1 , . . . , t n if and only if t 1 σ = . . . = t n σ. As is well known, any unifiable set of terms has a most general unifier (unique up to a renaming), denoted by mgu(t 1 , . . . , t n ). Note that in our simple case, all terms are of the form s i (t) where t ∈ {0} ∪ V. Thus any unifier of s i (t) and s j (s) where t, s ∈ {0} ∪ V, if it exists, is either empty or of one of the forms t → s j-i (s) (if t ∈ V and j ≥ i) or s → s i-j (t) (if s ∈ V, t = s and j < i). Notice that according to this definition, any set of purely equational clauses is equivalent to a linear arithmetic formula.

Remark 2.2. The notion of an s-interpretation slightly differs from (and is more restrictive than) the standard notion of a first-order interpretation because parameters are interpreted as natural numbers and not on an arbitrary domain. For instance, the clause set {n ≈ 0, n ≈ s(x)}, which is obviously satisfiable in the usual sense, is s-unsatisfiable, since the value of the parameter n must be either 0 or a term of the form s(x). Similarly, 0 and s are interpreted as free constructors (i.e. as the usual functions on N), thus for instance the clause set {n ≈ 0, n ≈ s(0)} is s-unsatisfiable, although it is satisfiable in the usual sense. Note that by definition, any clause of the form n ≈ u ∨ n ≈ v ∨ C, where u and v are not unifiable, is s-valid. For instance, n ≈ s(x) ∨ n ≈ x holds in any s-interpretation, since n cannot be equal to both s(t) and t for any t ∈ T .

This makes all the usual proof procedures incomplete (though still sound): for instance it is clear that the empty clause cannot be derived from the previous clause sets by the standard resolution or superposition calculus. In the following, we always refer to our new definitions of interpretations and models, unless otherwise specified. In particular, the properties of our calculus (i.e. soundness and completeness) are meant w.r.t. our particular semantics. Of course, if the considered formula contains no occurrence of n (i.e. no equational atom) then the notion of an s-interpretation coincides with the usual one, and in this case the obtained language is equivalent to a subclass of monadic first-order logic (the predicate symbols have only one argument and the set of function symbols is {0, s}). If, moreover, the formula contains no occurrence of 0 or s, then it is easy to check that it is equivalent to a purely propositional formula (in this case the indices are irrelevant).

Notice also that if the considered formula is purely equational (i.e. contains no propositional variable) then it is equivalent to a linear arithmetic formula, or, more simply, to an equational formula interpreted on the term algebra. This entails the following proposition.

Proposition 2.3. The satisfiability problem is decidable for finite purely equational clause sets.

Proof: By definition of the semantics, a purely equational clause set {C 1 , . . . , C k } is equivalent to the formula k i=1 ∀ x i C i where x i is the set of index variables in C i . The only symbols occurring in this formula besides the variables in x i ) are 0, s, ≈, ≈ and the parameters. Since 0 and s are interpreted as free constructors, {C 1 , . . . , C k } is s-satisfiable if and only if the formula ∃ n. k i=1 ∀ x i C i holds in the free term algebra, where n is the set of parameters in C 1 , . . . , C k . The satisfiability problem is well known to be decidable for such formulae (by using, e.g., the algorithm in [START_REF] Comon | Equational Problems and Disunification[END_REF], or any decision procedure for linear arithmetic [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt[END_REF][START_REF] Cooper | Theorem Proving in Arithmetic without Multiplication[END_REF]).

The calculus

Definition

Given two terms u and v, we write u v if and only if v = s i (u) for some i > 0 (0 and s(x) are incomparable). This strict ordering is extended into an ordering on index atoms as follows: p u q v if and only if u v.

We assume that a total strict ordering ≺ is given on the elements of Ω. The ordering ≺ is extended into a strict ordering on atoms as follows: a ≺ a if and only if either a a or there exists a term u such that a = p u , a = q u and p ≺ q. By definition, equational atoms are not comparable. Note that ≺ is stable under substitution, i.e. a ≺ a ⇒ aσ ≺ a σ, for every substitution σ. The orderings and ≺ are extended to index literals by ignoring negation symbols and to clauses by the multiset extension.

Let sel be a selection function mapping every clause C to a possibly empty set of selected index literals in C. We assume that sel satisfies the following conditions: for every clause C such that C idx = ∅, either sel(C) is a nonempty set of -maximal negative literals or sel(C) is the set of all ≺-maximal literals in C idx . In particular, since by definition sel(C) ⊆ C idx , equational literals are never selected, thus sel

(C) = ∅ if C idx = ∅.
For instance, consider the clause

C : n ≈ s(s(x)) ∨ ¬p x ∨ ¬p s(x) ∨ q s(x) ∨ r s(x)
and assume that p ≺ q ≺ r. Then p s(x) , q s(x) and r s(x) are -maximal, and r s(x) is ≺-maximal. The set of selected literals sel(C) can contain the literals ¬p s(x) or r s(x) (but not both) but neither ¬p x nor q s(x) . The resolution calculus is defined, as usual, by the rules depicted in Figure 1 (we externalize factorization for technical convenience). Note that the negative factorization rule will actually be useless in the rest of the paper. We present it for the sake of uniformity. We denote by Res(S) the set of clauses that can be deduced from (pairwise index variable disjoint renamings of) clauses in S by resolution or factorization in one step. A derivation from a clause set S is a sequence of clauses C 1 , . . . , C k such that for

p u ∨ p v ∨ C (p u ∨ C)σ ¬p u ∨ ¬p v ∨ C (¬p u ∨ C)σ
where: The following notion of a refutation differs from the usual one, indeed since no rule can be applied on the equational part of the clauses, these literals cannot be eliminated: Definition 3.1. A refutation of S is a derivation from S of a finite s-unsatisfiable set of purely equational clauses.

σ = mgu(u, v), p u σ is selected in (p u ∨p v ∨C)σ
The satisfiability of such a set can be tested by Proposition 2.3.

Basic properties of the calculus

It is straightforward to check that the above rules are sound, i.e., that the conclusions are logical consequences of the premises. Proposition 3.2. Let S be a set of clauses. Then S |= s Res(S).

We prove a weak form of refutational completeness. A first step towards this proof is to notice that the calculus is complete for parameter-free clause sets: Proposition 3.3. Let S be a saturated set of parameter-free clauses. If S is s-unsatisfiable then ∈ S.

Proof: It is enough to observe that, when the clauses under consideration contain no equational literals, this calculus coincides with the ordinary resolution calculus. Theorem 3.4. Let S be a saturated set of clauses. If S is s-unsatisfiable then there exists a (possibly infinite) set of purely equational clauses S ⊆ S that is s-unsatisfiable.

Proof: Let I be an s-interpretation, let S g be the set of ground instances of the clauses in S. Consider the set of ground clauses S I obtained from S g by:

• deleting every clause containing an equational literal that is true in I,

• removing all equational literals in the remaining clauses.

By construction, S I contains no equational literal, hence no parameter, and if S I admits a model J, then obviously the s-interpretation K that coincides with I on all parameters and with J on all ground indexed atoms is an s-model of S. Thus, by hypothesis, S I must be unsatisfiable. We verify that S I is saturated in order to use Proposition 3.3.

By hypothesis, S is saturated. Since the notion of saturatedness only depends on ground instances and since resolution of ground clauses generates only ground clauses, it is clear that S g is also saturated. Let p u ∨ C and ¬p u ∨ D be two clauses in S I on which the resolution rule applies. By definition, S g contains two clauses p u ∨ C ∨ C and ¬p u ∨ D ∨ D , where C , D are purely equational clauses that are false in I. Since S g is saturated, there exist This proves that Res(S I ) S I and hence that S I is saturated. By Proposition 3.3, we deduce that ∈ S I , which means that S contains a purely equational clause C I that is false in I. We then take for S the set of all such C I 's for every s-interpretation I: S is indeed s-unsatisfiable and included in S.

m clauses E 1 , . . . , E m ∈ S g such that E 1 , . . . , E m |= s C ∨ D ∨ C ∨ D and E 1 , . . . , E m C ∨ D ∨ C ∨ D .
In the case where S is finite, Proposition 2.3 can be used to test its satisfiability. However, Theorem 3.4 does not imply semi-decidability because S may well be infinite.

Example 3.5. Consider the set S = {n ≈ x ∨ p x , p y ∨ ¬p s(y) , ¬p 0 }, which formalizes the following statements:

• p n holds,
• if p i+1 holds, then so does p i ,

• p 0 does not hold.

It is clear that S is s-unsatisfiable. Yet, this cannot be detected in finite time by the calculus, which generates an infinite set of purely equational clauses of the form n ≈ s i (0):

1 n ≈ x ∨ p x (given) 2 p y ∨ ¬p s(y) (given) 3 ¬p 0 (given) 4 n ≈ s(y) ∨ p y (resolution 1, 2, x → s(y)) 4 n ≈ s(y ) ∨ p y (renaming, 4) 5 n ≈ 0 (resolution 1, 3, x → 0) 6 n ≈ s(0) (resolution 4, 3, y → 0) 7 n ≈ s(s(y)) ∨ p y (resolution 4 , 2, y → s(y)) 8 n ≈ s(s(0)) (resolution 7, 3, y → 0) . . .
This set of clauses is clearly s-unsatisfiable, but every finite subset of it is s-satisfiable.

A natural way of verifying that this set is s-unsatisfiable would be to realize that clauses 1 and 2 generate clause 4, which states that p n-1 holds, and this clause is identical to clause 1, up to a shift of parameter n. By iteration, it is possible to generate any clause of the form n ≈ s k (x) ∨ p x for k ∈ N, stating that p n-k holds. Then the infinite descent principle implies that p 0 must also hold, a contradiction. It turns out that the detection of such a loop between clauses 1 and 4 implies that it is not necessary to consider an arbitrary value for n, and that it can safely be assumed that n < 3. Indeed, it can be shown that any s-interpretation mapping n to an integer greater than 3 can be transformed into another one mapping n to a strictly smaller integer, such that both s-interpretations agree on the truth value of S. The translation into clausal form of this remark yields the purely equational clause n ≈ s(s(s(x))), and the calculus can be used to prove that S ∪ {n ≈ s(s(s(x)))} is s-unsatisfiable in finite time. Indeed, we have shown that the calculus generates the following set of clauses: {n ≈ 0, n ≈ s(0), n ≈ s(s(0))} (meaning that n must be distinct from 0, 1 and 2). If one adds to this set the clause n ≈ s(s(s(x))) (i.e. n < 3), one gets an s-unsatisfiable set of purely equational clauses. The unsatisfiability of this set can be tested by using existing decision procedures for linear arithmetic.

In what follows, we generalize this observation to introduce a rule that will permit to prune infinite derivations and thus obtain a refutationally complete calculus for schematic clauses. After restricting the form of the clauses under consideration, which in particular can only admit a single parameter n, we define a loop-detection rule that is based on so-called levels of sets of clauses. We show that once such a loop has been detected, a pruning clause representing an upper-bound constraint on the parameter n can safely be added to the considered set of clauses, and termination will be ensured, provided a fair strategy is applied for the calculus.

A restriction of the language

In order to conveniently exploit the properties of the calculus, we restrict ourselves to a particular class of clause sets. The clauses in this class have a simple structure that will be used to achieve refutational com-pleteness, and, as shown in Section 5, no loss of expressiveness is entailed for our purpose. Informally the restrictions we impose to the sets of clauses are the following:

• The equational part of the clauses must be negative.

• The non-equational part of any clause is of a limited depth (0 or 1).

• The clauses contain at most one index variable and clauses containing a variable cannot contain any ground term (i.e. no occurrence of constant symbol 0). For instance, the clauses p x ∨ p y and p x ∨ q 0 do not satisfy these restrictions.

Formally, this particular class is based on so-called t-clauses:

Definition 4.1. Let t ∈ {0} ∪ V. A clause C is a t-clause if and only if every indexed atom occurring in it is of the form p s i (t) for some i ∈ N. Proposition 4.2. 1. If C is a t-clause, with t ∈ V ∪ {0} and σ is flat then Cσ is a tσ-clause. 2. If C, D are t-clauses then C ∨ D is a t-clause.
Definition 4.3. A clause C is normalized if and only if there exists a term t ∈ V ∪ {0} such that the following conditions hold:

• C eq is either empty or of the form n ≈ s k (t) with k ≥ 0.

• C idx is a t-clause of depth 0 or 1.

• If t = 0 then depth(C idx ) = 0.
In particular, these conditions ensure that the indices occurring in the clause set are of the form 0, x or s(x), where x is a variable. The last condition dismisses clauses such as n ≈ 0 ∨ p s(0) , because p s(0) is a 0-clause of depth 1.

A set of clauses S is normalized if and only if the two following conditions hold:

• S contains at most one parameter (always denoted by n in what follows).

• Every clause in S is normalized.

Example 4.4. The clauses p x ∨¬p s(x) , n ≈ s(s(x))∨p x and n ≈ 0∨q 0 are normalized, but n ≈ 0∨p s(0) , n ≈ s(x) ∨ ¬p 0 ∨ q x and p s(s(x)) are not. The clause n ≈ 0 ∨ p s(0) indeed falsifies the third condition because p s(0) is of depth 1, and the other clauses falsify the second condition: there is no term t such that n ≈ s(x) ∨ ¬p 0 ∨ q x is a t-clause, and p s(s(x)) is an x-clause of depth 2. The set of clauses in Example 3.5 is normalized.

Remark 4.5. If S is normalized, then it is easy to check that the purely equational clauses contained in S must be of the form n ≈ s k (t), where t is either 0 or a variable. Thus any such clause is equivalent to n ≈ k or n < k. Therefore, deciding whether a finite set of purely equational clauses contained in S is s-unsatisfiable or not is much easier than solving general Presburger formulae: it suffices to detect whether there exists a natural number k such that S contains a clause of the form n ≈ s k (x), and for every i

∈ [0, k -1], a clause of the form n ≈ s i (0).
The following proposition is a direct consequence of the definitions of the ordering ≺ and of normalized clauses.

Proposition 4.6. Every normalized non-tautological clause C contains at most one ≺-maximal index literal l. If the index of l is a variable, then depth(C idx ) = 0. Proposition 4.7. If the Factorization rule can be applied to a normalized clause, then this application is trivial, i.e., it consists in removing a duplicate literal.

Proof: Assume the Factorization rule can be applied to a normalized clause

p u ∨ p v ∨ C (the proof is identical if it is applied to a clause ¬p u ∨ ¬p v ∨ C ).
By definition, u and v are either both ground or both of the form s i (x) and s j (x) for some variable x. In both cases, u and v are unifiable if and only if u = v, in which case their mgu is empty. Therefore, the rule simply removes a duplicate literal.

We introduce the notion of level which is a measure on normalized clauses. As we shall see, the level of normalized clauses cannot decrease with inferences.

Definition 4.8. The level of a normalized clause is an element of N ∪ {⊥}, defined as follows:

• If C eq = then level(C) def = ⊥. • If C eq = then level(C) def = depth(C eq ) -depth(C idx ) + 1.
If i ∈ N ∪ {⊥}, then S| i denotes the set of clauses in S of level i. If I is a subset of N ∪ {⊥}, then S| I denotes the set of clauses whose levels are in I.

In other words, a normalized clause of level ⊥ is parameter-free, and a normalized clause of level j ∈ N is of the form n ≈ s j+ε-1 (t) ∨ C, where C is a t-clause of depth ε.

Example 4.9. The levels of n ≈ s(0) ∨ p 0 , n ≈ s(s(x)) ∨ p s(x) and n ≈ s(x) ∨ p x are all equal to 2. For any parameter-free and normalized clause C, the level of n ≈ 0 ∨ C is 1, that of n ≈ s(0) ∨ C is 2, etc., since C necessarily has depth 0 in this case. The level of n ≈ s(s(x)) ∨ p x is 3, and so is the level of its instance n ≈ s(s(s(y))) ∨ p s(y) ; the level of n = s(s(x)) ∨ p s(x) is 2.

Example 4.10. We give the level of each clause occurring in the partial derivation of Example 3.5:

1. level(n ≈ x ∨ p x ) = 1 2. level(p y ∨ ¬p s(y) ) = ⊥ 3. level(¬p 0 ) = ⊥ 4. level(n ≈ s(y) ∨ p y ) = 2 5. level(n ≈ s(y ) ∨ p y ) = 2 6. level(n ≈ 0) = 1 7. level(n ≈ s(0)) = 2 8. level(n ≈ s(s(y)) ∨ p y ) = 3 9. level(n ≈ s(s(0))) = 3
Intuitively, a clause of level ⊥ expresses either some universal property such as ∀x ¬p x ∨ p s(x) or a ground property, e.g. p 0 , p s(0) , i.e., in general, a property that is independent of a parameter n. A clause of a level distinct from ⊥ is of the form n ≈ s k (t) ∨ C where the only indices occurring in C are t or s(t). Such a clause can be viewed as an implication: n ≈ s k (t) ⇒ C. If t = 0 then the clause states a ground property that must be true when n is equal to k. If t is a variable, then the clause expresses a property for t = n -k, in case n -k exists. This can be read as n ≥ k ⇒ C{t → n -k}.

We order the levels in N ∪ {⊥} by using the usual ordering on natural numbers and by assuming that

⊥ < i for every i ∈ N. Thus if i is a natural number then the interval [⊥, i] (resp. [⊥, i[) denotes the set {⊥} ∪ [0, i] (resp. {⊥} ∪ [0, i[). Definition 4.11. A set of clauses is k-normalized if it is normalized and the level of every clause in S is in [⊥, k].
Proposition 4.12. For every k ∈ N ∪ {⊥}, the number of normalized clauses of level k on a given finite signature Ω is at most 2 4|Ω|+1 , up to a renaming and up to the duplication of literals.

Proof: This is an immediate consequence of the fact that any normalized clause of level k is of the form n ≈ s k-ε+1 (t) ∨ C or C, where C is a t-clause of depth ε ∈ {0, 1}, thus every literal in C is of the form p t , ¬p t , p s(t) or ¬p s(t) , for some p ∈ Ω. Since t ∈ {0} ∪ V, we have the result.

The following lemma states that the class of normalized clauses is preserved by the inference rules. Proof: Proposition 4.7 proves this is the case for the Factorization rule. Let C be a non-valid clause deduced from two normalized clauses D 1 and D 2 by resolution. We assume as usual that the variables are renamed apart so that D 1 and D 2 share no variables. By definition, D idx 1 and D idx 2 are of the form p u 1 ∨ D 1 and ¬p u 2 ∨ D 2 where u 1 and u 2 are unifiable; furthermore, since S is normalized, there exist terms t 1 and t 2 such that

D idx 1 is a t 1 -clause and D idx 2 a t 2 -clause. For i = 1, 2, let D i def = D eq i ; by hypothesis, D i is either empty or of the form n ≈ s k i (t i ). Thus C is of the form (D 1 ∨ D 2 ∨ D 1 ∨ D 2 )σ, where σ = mgu(u 1 , u 2 )
. By definition, any atom occurring in D i is of the form q t i or q s(t i ) , hence u i is either t i or s(t i ), and σ must be of one of the following forms:

∅, {t 1 → t 2 }, {t 2 → t 1 }, {t 2 → s(t 1 )} (when t 2 ∈ V and t 1 ∈ V ∪ {0}), {t 1 → s(t 2 )} (when t 1 ∈ V and t 2 ∈ V ∪ {0}).
If σ is empty or of the form

t 2 → t 1 or t 1 → t 2 , then t 1 σ = t 2 σ 1 . Since σ is flat, by Proposition 4.2 (1), D i σ is a t i σ-clause, and by Proposition 4.2 (2), D 1 σ ∨ D 2 σ is a t 1 σ-clause. Assume that D 1 and D 2 are not empty. Then D i must be of the form n ≈ s k i (t i ). If k 1 = k 2 , then C contains the disjunction n ≈ s k 1 (t 1 σ) ∨ n ≈ s k 2 (t 2 σ). Since t 1 σ = t 2 σ and k 1 = k 2 , s k 1 (t 1 σ
) and s k 2 (t 2 σ) are not unifiable and C is valid. Since we assumed C is not valid, (D 1 ∨ D 2 )σ is either empty or of the form n ≈ s k 1 (t 1 σ), thus C is normalized (modulo factoring, since this literal may occur twice in C).

Assume that σ is {t 2 → s(t 1 )}, the proof is similar if σ is {t 1 → s(t 2 )}. If D 2 σ contains an atom of the form q s(t 2 ) then by definition of the ordering, p t 2 q s(t 2 ) and by definition of the selection function, the literal ¬p t 2 cannot be selected, which is impossible. Hence every atom in D 2 σ is of the 1 Note that if σ is empty then u1, u2 are ground thus, since D1, D2 are normalized, we must have u1 = u2 = t1 = t2 = 0. form q t 2 σ = q s(t 1 ) , and is therefore a t 1 -clause. It is clear that D 1 σ is a t 1 -clause, since σ is the identity on D 1 . Thus, by Proposition 4.2 (2), D 1 σ ∨ D 2 σ is also a t 1 -clause. Assume that D 1 and D 2 are not empty and that

k 1 = k 2 + 1. Then C contains the disjunction n ≈ s k 1 (t 1 σ) ∨ n ≈ s k 2 (t 2 σ). Since t 2 σ = s(t 1 ) and k 1 = k 2 + 1, s k 1 (t 1 σ
) and s k 2 (t 2 σ) are not unifiable, hence C is valid. Since C was assumed not to be valid, (D 1 ∨ D 2 )σ is either empty or of the form n ≈ s k 2 +1 (t 1 ) and C is normalized (modulo factoring).

We also relate the level of any clause to that of its parents: intuitively, the levels of the clauses generated by the calculus can never decrease. This is obvious for the Factorization rule which removes duplicate literals (see Proposition 4.7), the following lemma proves the result for the resolution rule. Lemma 4.14. Let S be a set of normalized clauses. Let C be a non-valid clause of level j ∈ N in Res(S), deduced from parent clauses D 1 , D 2 in S of levels k 1 , k 2 ∈ N∪{⊥} respectively. The following conditions hold:

• k 1 , k 2 ∈ {⊥, j, j -1}. • If C is ground then k 1 , k 2 ∈ {⊥, j}. • If k 1 = ⊥ and k 2 = ⊥ then k 1 = k 2 . • (k 1 , k 2 ) = (⊥, ⊥).
Proof: The last item is immediate since the rules cannot create new equational literals and C is of level j = ⊥ by hypothesis. By definition, there exists a term t ∈ V ∪ {0} such that C is of the form n ≈ s j-1+ε (t) ∨ C where C is a t-clause of depth ε (recall that j = ⊥ by hypothesis). Thus, D i is either parameter-free or of the form n ≈ s k i -1+ε i (t i ) ∨ D i where D i is a t i -clause of depth ε i , and s j-1+ε (t) = s k i -1+ε i (t i )σ, where σ is the mgu of two terms u 1 and u 2 occurring in selected literals in D 1 and D 2 respectively.

The terms u 1 and u 2 are of the form 0, x i or s(x i ) where x i is a variable. Several cases are distinguished according to the form of σ.

• If σ is empty, then u 1 = u 2 = 0. In this case, D 1 , D 2 are ground, hence C is also ground. Furthermore, if D i is not parameter-free then j -1 + ε = k i -1 + ε i . By the definition of closed normalized clauses, ε = ε i = 0, hence j = k i . Therefore, if k 1 , k 2 = ⊥ then we must have k 1 = k 2 . • If σ is of the form x 1 → x 2 , x 2 → x 1 , x 1 → 0 or x 2 → 0, then D idx 1 and D idx 2 must be of the same depth. Assume that k i = ⊥. Since σ is flat, j -1 + ε = k i -1 + ε i , thus k i = j + ε -ε i . If ε = 0 then k i ∈ {j, j -1}. If ε = 1 then, by definition, C is of depth 1.
Since every literal in C occurs either in D 1 σ or in D 2 σ, one of them, say D 1 σ, is of depth 1 (and D 2 σ is of depth 0 or 1). But σ is flat, therefore, in this case, D 1 is also of depth 1 and we have

ε i = ε = 1. Therefore, k i = j. Thus, in all cases, k 1 , k 2 ∈ {⊥, j, j -1}, and if k 1 , k 2 = ⊥ then k 1 = k 2 . If C is ground, then either u 1 = 0 or u 2 = 0, hence ε 1 = ε 2 = 0. But, since C is ground, ε = 0, hence k 1 , k 2 ∈ {⊥, j}. • If σ is of the form x 1 → s(x 2 ), then u 1 = x 1 and u 2 = s(x 2 ). In this case C is not ground. Assume that k 1 = ⊥. Then j -1 + ε = k 1 -1 + (ε 1 + 1), thus k 1 = j + ε -ε 1 -1. But since u 1 is maximal, necessarily ε 1 = 0, which implies that k 1 = j + ε -1 ∈ {j -1, j}. If k 2 = ⊥ then j -1 + ε = k 2 -1 + ε 2 , thus k 2 = j + ε -ε 2 . Furthermore, since u 2 = s(x 2 ) occurs in D 2 , necessarily ε 2 = 1 and k 2 = j + ε -1 ∈ {j -1, j}.
• The case where σ is of the form x 2 → s(x 1 ) is symmetrical.

Expressive power

Although the class of normalized clause sets is strongly restricted from a syntactic point of view, it is actually quite expressive. This section is devoted to showing how literals that are outside the class can be encoded into normalized clause sets.

Encoding a translation on indices

We first consider atoms of the form p s k (x) , where k ≥ 2. Such atoms are encoded by new predicate symbols p k x , with the intended meaning p k x ⇔ p s k (x) . The following axioms ensure that p k x has the intended s-interpretation:

A k def = {p l x ⇔ p l-1 s(x) , p 0 x ⇔ p x | 0 < l ≤ k}
where x ⇔ y is an abbreviation for {¬x ∨ y, x ∨ ¬y}. Note that A k is finite and normalized. The following result is proved by a straightforward induction on l:

Proposition 5.1. For every l ∈ [0, k], A k |= s p l x ⇔ p s l (x) .
Example 5.2. The s-unsatisfiable clause set:

{¬even x ∨ even s(s(x)) , even(0), ¬odd x ∨ odd s(s(x)) , odd s(0) , n ≈ x ∨ ¬even x , n ≈ x ∨ ¬odd x }
is not normalized, since it contains non-equational atoms of depth 2. According to our previous transformation algorithm, it would be encoded as the following normalized set of clauses:

¬even x ∨ even 1 s(x) ¬even 1 x ∨ even s(x) even 1 x ∨ ¬even s(x) ¬odd x ∨ odd 1 s(x) ¬odd 1 x ∨ odd s(x) odd 1 x ∨ ¬odd s(x) even(0) odd 1 (0) n ≈ x ∨ ¬even x n ≈ x ∨ ¬odd x

Encoding inequalities and equalities

The formula x+l > ε•n+k (with l, k ∈ N, ε ∈ {0, 1}) is encoded by a predicate q l,ε,k x , whose semantics are defined by the following axioms A l ,k :

1 q l,ε,k x ⇔ q 0,ε,k s l (x) 2 q 0,ε,k+1 s(x) ⇔ q 0,ε,k x 3 ¬q 0,ε,k 0 4 q 0,0,0 s(x) 5 n ≈ x ∨ q 0,1,0 s(x) 6 n ≈ x ∨ ¬q 0,1,0 x 7 q 0,1,0 s(x) ∨ ¬q 0,1,0 x where l ∈ [0, l ], k ∈ [0, k ] and ε ∈ {0, 1}.
Again, A l ,k is finite. It is not normalized due to the index s l (x) in the first axiom, but the transformation of Section 5.1 yields an equivalent normalized formulation.

Proposition 5.3. Let I |= s A l ,k . For every (l, ε, k) ∈ [0, l ] × {0, 1} × [0, k ], we have I |= s q l,ε,k x ⇔ x + l > ε • n + k.
Proof: Assume that l = k = 0. If ε = 0 then the s-interpretation of q l,ε,k is fixed by the third and fourth axioms and we have indeed q 0,0,0 s(x) (i.e. s(x) > 0) and ¬q 0,0,0 0 (i.e. 0 > 0). If ε = 1, then the s-interpretation of q l,ε,k is fixed by the fifth and sixth axioms that state that we have q 0,1,0 s(x) if x = n (i.e. s(n) > n) and ¬q 0,1,0 x if x = n (i.e. n > n). Furthermore, the last axiom ensures that q 0,1,0 s(x) holds if q 0,1,0 x holds. Since q 0,1,0 s(n) holds, this implies that q 0,1,0 s(s(n)) ,q 0,1,0 s(s(s(n))) , . . . hold, and since ¬q 0,1,0 n does not hold, this implies that q 0,1,0 n-1 ,q 0,1,0 n-2 , . . . do not hold. Thus q 0,1,0

x is true if and only if x ≥ s(n). By using the second and third axioms we can show by a straightforward induction on x that q 0,ε,k x is equivalent to q 0,ε,k-x 0 if x < k and to false otherwise. Then the first axiom states that q l,ε,k x is equivalent to q 0,ε,k x+l .

The formula x + l ≤ ε.n + k can be easily encoded as

x + l + 1 > ε.n + k. Then x + l ≈ ε.n + l can be written as x + l + 1 ≥ ε.n + l ∧ x + l ≤ ε.n + l + 1.
Example 5.4. The formula x ≤ n ⇒ p x can be encoded as the following normalized set:

q 0,1,0 x ∨ p x ¬q 0,1,0 0 n ≈ x ∨ q 0,1,0 s(x)
n ≈ x ∨ ¬q 0,1,0 x q 0,1,0 s(x) ∨ ¬q 0,1,0

x

The atom q 0,1,0

x holds if and only if x > n.

Encoding schemata with several parameters

The restriction to one parameter entails no loss of generality. Indeed, let S be a clause set with k parameters n 1 , . . . , n k . We introduce a new parameter n (which encodes the max of the n i 's). The formula x > n l is encoded using an atom r l x , axiomatized by the following set of clauses A :

¬r l x ∨ r l s(x) ¬r l 0 n ≈ x ∨ r l s(x) where l ∈ [1, k].
The clause ¬r l x ∨ r l s(x) encodes the fact that x > n l ⇒ s(x) > n l . The clause ¬r l 0 states that the formula (0 > n l ) does not hold (i.e. that we have 0 ≤ n l ) and the clause n

≈ x ∨ r l s(x) states that s(n) > n l (since n = max{n l | l ∈ [1, k]}).
Notice that the resulting formula is normalized.

Proposition 5.5. If I |= s A then for every l ∈ [1, k] there is exactly one natural number n l such that I |= s r l

x if and only if x > n l . Furthermore, n l ≤ I(n).

Proof: Let n l be the least natural number such that I |= s r l s(n l ) . Such an n l exists and must be lower or equal to I(n), since r l s(n) holds (by the third axiom). By minimality of n l , r l n l can only hold if n l = 0, which is impossible since I |= s ¬r l 0 (by the second axiom). Then by using the first axiom we show that I |= s r l

x for every x > n l and that I |= s ¬r l x for every x ≤ n l .

Then the formula x ≈ n l is written x + 1 > n l ∧ x > n l .

Example 5.6. The formula p m ∧ ¬p k (meaning that there is a natural number such that p is true and one for which it is false) is written as follows (n is a new parameter denoting the max of m and k).

¬r m x ∨ r m s(x) ¬r m 0 n ≈ x ∨ r m s(x) ¬r k x ∨ r k s(x) ¬r k 0 n ≈ x ∨ r k s(x) r m x ∨ ¬r m s(x) ∨ p x r k x ∨ ¬r k s(x) ∨ ¬p x For instance, r k
x holds if and only if x > k, thus the last clause states that if x > k and s(x) > k (i.e. if x = k) then ¬p x holds. It is thus equivalent to ¬p k .

Inductive definitions

Now, consider an inductive definition: φ 0 ≡ B and φ k+1 ≡ I(k) if k ≥ 0 where B and I denotes formulae and where I(k) contains atoms of the form p k or p s(k) or inductively defined formulae ψ k (with possibly φ = ψ). This definition can be easily expressed in our formalism by considering every such formula φ as a predicate symbol:

φ 0 ⇔ B φ s(x) ⇔ I(x)
One gets a 1-normalized clause set by translation into clausal form. More complex inductive definition may be encoded in the same way. In particular, formulae of the form b i=a φ i (where b -a ≥ 0) are easily encoded by an atom ψ b-a+1 to be interpreted as b-a+1 x=1 φ x-1+a defined as follows:

ψ 0 ⇔ false ψ x+1 ⇔ φ x-1+a ∨ ψ x
After translation into clausal normal form and after encoding the index translation (i.e. after encoding the atom φ x-1+a by using only indices of depth 1) as explained in Section 5.1, one gets a normalized clause set.

Example 5.7. The formula n i=0 p i ∧ n i=1 ¬p i can be encoded as follows:

n ≈ x ∨ q s(x) n ≈ x ∨ r x ¬q 0 ¬q s(x) ∨ p x ∨ q x q s(x) ∨ ¬p x q s(x) ∨ ¬q x ¬r s(x) ∨ ¬p x ¬r s(x) ∨ r x ¬r s(x) ∨ p x ∨ ¬r x

Regular schemata

Using the previous transformations it is easy to prove that every regular schema (in the sense of [START_REF] Aravantinos | Decidability and Undecidability Results for Propositional Schemata[END_REF]) can be encoded into a normalized clause set, i.e. that for every regular schema φ one can construct a normalized clause set S such that φ and S are equi-s-satisfiable in a strong sense: every s-model of S is also a model of φ and every s-model of φ can be extended into a model of S. Furthermore, the size of S is linear w.r.t. that of φ (if natural numbers are encoded as unary terms in the original schema 2 and if a structural-preserving transformation is used to compute clausal forms). Furthermore, normalized clause sets allow one to express properties that cannot be stated as regular schemata, for instance the formula ∞ x=0 p x is easily expressed by the normalized clause set {p x } but it is not a regular schema (due to the unbounded conjunction).

Loop detection

In this section we extend the calculus proposed in Section 3 by defining a loop detection rule that is capable of pruning infinite derivations. To help the reader grasp the following definitions and lemmata, we first provide an informal high-level description of the rule. Let S be a clause set. The set of clauses S = {C | S C} generated from S can be partitioned into an infinite sequence of clause sets S | ⊥ , S | 1 , . . . , S | k ,. . . , where for every k ∈ N ∪ {⊥}, S | k contains exactly the clauses of level k in S (see Definition 4.8). Due to ordering restrictions, the resolution rule cannot increase the depth of the non-equational part of the clause, which is therefore bounded (this depth is at most 1). Consequently, there are only finitely many distinct clauses, up to a shift of parameter n. For instance, n ≈ x ∨ p x and n ≈ s(s(x)) ∨ p x are identical, up to the shift n → n -2. Thus, there must exist, by the pigeonhole principle, two natural numbers i and j > 0 such that the set of clauses generated at level i is equivalent to the set of clauses generated at level i + j, up to a shift on the parameter n. If, moreover, the considered clause sets are saturated, this implies that the clause sets of the next levels i + 1 and i + j + 1 will be also equivalent, yielding a cycle in the derivation. We will show that, under some particular conditions, the existence of such a cycle in the derivation permits to deduce an upper-bound on the value of the parameter n: if S is s-satisfiable then it has a model I such that I(n) < i + j. The intuition is that if a model I such that I(n) > i + j exists, then it is possible to obtain another model J such that J(n) = I(n) -j, by applying the translation n → n -j on I. This implies that the constraint n < i + j (written n ≈ s i+j (x) in clausal form) can be safely added to S . It is then clear that every clause of a level strictly greater than i + j is redundant w.r.t. n < i + j, since n ≈ s i+j (t) ∨ C is obviously subsumed by n ≈ s i+j (x). Consequently, once the pruning clause n < i + j has been generated, only finitely many non-redundant clauses can be deduced.

We now formalize those intuitive ideas. We begin by slightly restricting the notion of redundancy (see Definition 4.8 for the meaning of S| I ): Definition 6.1. A clause C is level-redundant w.r.t. a set of clauses S (written C l S) if and only if for every ground substitution σ of domain var(C) there exist clauses C 1 , . . . , C m in S and ground substitutions θ 1 , . . . , θ m such that:

• If C is not ground then neither are C 1 , . . . , C m .
• The clauses in C 1 , . . . , C m are either of level ⊥ or of the same level as C.

• C 1 θ 1 , . . . , C m θ m |= s Cσ and C 1 θ 1 , . . . , C m θ m Cσ.
If S is a set of clauses, then we write S l S if and only if ∀C ∈ S , C l S. For every i ∈ N ∪ {+∞, ⊥}, a set of clauses S is saturated up to level i if and only if Res(S| [⊥,i[ ) l S.

For instance, p x is redundant w.r.t. {p 0 , p s(x) } (because, since the signature only contains the symbols 0 and s, every instance of p x is either an instance of p 0 or an instance of p s(x) ) but not level-redundant (since p 0 is ground and p x is not). Notice that p 0 and p s(x) are also both redundant and level-redundant w.r.t. {p x }. The clause n ≈ s(x) ∨ p x ∨ p s(x) is redundant w.r.t. {n ≈ s(x) ∨ p x } but not level-redundant since level(n ≈ s(x) ∨ p x ∨ p s(x) ) = 1 and level(n ≈ s(x) ∨ p x ) = 2.

As we shall see, ground clauses will be dismissed when applying the loop detection rule (see Definition 6.9 and also Condition 3 in Lemma 6.6). Thus we avoid using them to delete non-ground clauses (first item in Definition 6.1). The following property is an immediate consequence of Definition 6.1:

Proposition 6.2. If C is a clause of level i that is level-redundant w.r.t. a set of clauses S, then S| i ∪ S| ⊥ |= s C.
S = {n ≈ s(s(x)) ∨ ¬p x ∨ p s(x) , n ≈ s(x) ∨ q x , n ≈ 0 ∨ p 0 , ¬r x }
We have for example:

shift(S, 0) = {n ≈ s(s(x)) ∨ ¬p x ∨ p s(x) , n ≈ s(x) ∨ q x }, shift(S, 1) = {n ≈ s(s(s(x))) ∨ ¬p x ∨ p s(x) , n ≈ s(s(x)) ∨ q x }, shift(S, 2) = {n ≈ s(s(s(s(x)))) ∨ ¬p x ∨ p s(x) , n ≈ s(s(s(x))) ∨ q x }.
Note that ¬r x or n ≈ 0 ∨ p x cannot occur in shift(S, j) because they contain no literal of the form n ≈ s i (x), where x ∈ V. Lemma 6.6 will set the foundations for the definition of the loop detection rule. This lemma applies when we detect that the clauses of a certain level i in S are logically entailed by those of a level i + j > i, up to a shift on parameter n. This means that any s-model of S| i+j is also a model of S| i , up to the shift n → n -j. If we assume 3 that S| i |= s S| [i,∞[ , this entails that any s-model of S| i+j is also a model of S| [i,∞[ up to the shift n → n -j. For any model I of S such that I(n) ≥ i + j, it is thus possible to construct an s-interpretation J such that J(n) = I(n) -j < I(n), and which coincides with I for S| [i,∞[ . Then, if we assume further that S is saturated up to level i and does not contain the empty clause, it is possible to show that this s-interpretation can be extended into an s-model of S. Thus, satisfiability is preserved when the value of n is constrained to be strictly lower than i + j. As explained earlier, adding this assertion to S makes every clause of a level greater than i + j redundant since it is subsumed by n < i + j. Definition 6.5. Given a parameter n and an integer l, we write n < l as a shorthand for the clause n ≈ s l (x) and call such a clause a pruning clause.

Given a set of clauses S, a pruning clause C is compatible with S if S is s-satisfiable exactly when S ∪ {C} is. Lemma 6.6. Let S be a set of normalized clauses of parameter n and assume i, j are natural numbers satisfying the following conditions:

1. S is saturated up to level i.

S|

i ∪ S| ⊥ |= s S| [i,∞[ .

S| i contains no ground clause.

4. j = 0.

S|

⊥ ∪ S| i+j |= s shift(S| i , j).
Then n < i + j is compatible with S.

Proof: Let I be an s-interpretation satisfying S. W.l.o.g. we assume that the valuation of n in I is minimal (w.r.t. the usual ordering on natural numbers), i.e. for every s-interpretation J such that J(n) < I(n), we have J |= s S. Suppose that I |= s n < i+j, i.e., that I(n) ≥ i+j (which implies that I(n) > 0 since j = 0 by assumption). We construct an s-interpretation J as follows:

• J(n) def = I(n) -j. By Condition 4, this implies that J(n) < I(n) thus by hypothesis on the minimality of the valuation of n in I, J |= s S.

• The value of the ground atoms p k (for k ∈ N) is defined by induction on the ordering ≺:

-If k ≤ I(n) -i -j + 1 then J(p k ) def = I(p k ).
-If k > I(n) -i -j + 1, then assume, by induction, that J(q k ) is defined for every atom q k such that q k ≺ p k . We set the value of J(p k ) to true if and only if S| [⊥,i[ contains a clause that admits a ground instance of the form p k ∨ C, such that all equational atoms in C are false in J and for all indexed atoms q in C, q ≺ p k , and J |= s C (this last condition is similar to the model construction method used for proving the refutational completeness of the resolution calculus, see for instance [START_REF] Bachmair | Resolution Theorem Proving[END_REF]).

Since i ,j). By definition, D is of the form n ≈ s i-1+ε (t)∨D , where D is a t-clause of depth ε. But D is not ground by Condition 3, thus t must be a variable x. This implies that shift(S| i , j) contains the clause n ≈ s i-1+ε+j (x) ∨ D , which is true in I. Since J |= s Dθ by hypothesis, necessarily J(n) = i-1+ε+k, and Note that D cannot be the empty clause since otherwise S would be s-unsatisfiable. If D is purely equational then D must be of the form n ≈ s l (t) for some l < i and t ∈ V ∪ {0}, because D ∈ S| [0,i[ and D is normalized. Then D is equivalent either to n < l (if t ∈ V) or to n = l (if t = 0). In the first case, we have I |= s D, which is impossible since I is an s-model of S and D ∈ S| [⊥,i] ⊆ S. In the second case, since l < i and J(n) = I(n) -j ≥ i we deduce J |= s D, a contradiction since we assumed J |= s D.

S| i ∪ S| ⊥ |= s S| [i,
I(n) = J(n)+j = i-1+ε+k +j. By hypothesis I |= s (n ≈ s i-1+ε+j (x) ∨ D )θ,
We thus assume D contains at least one index literal, and denote by l u the maximal index literal in D (which is unique by Proposition 4.6). D is of the form l u ∨ D ∨ D , where D is parameter-free, D is purely equational (any of them could be empty), and for all literals l ∈ D θ, l l u θ. By definition of the ordering ≺, this implies that the index of every literal l ∈ D θ is less or equal to uθ.

We distinguish two cases depending on the value of uθ.

• If uθ ≤ I(n) -i -j + 1, then every index in D θ is also less or equal to I(n) -i -j + 1. By construction of J, this implies that I and J coincide on (l u ∨ D )θ. Thus, if I satisfies (l u ∨ D )θ, then so does J, and this case is impossible, since J |= s Dθ. Hence, I |= s (l u ∨ D )θ, so that necessarily, I |= s D θ. By hypothesis, D is a normalized t-clause in S| [0,i[ that is not valid in J, hence D must be of the form n ≈ s m (t), where t ∈ V ∪ {0}, and if ε stands for the depth of

l u ∨ D , then level(D) = m -ε + 1 < i. Since J |= s D θ, either J(n) = m (if t = 0), or J(n) = m + k (if t = x); but the first case is impossible because I(n) ≥ i + j by hypothesis and J(n) = I(n) -j > i > m by construction. Thus, J(n) = m + k, so that k = J(n) -m > J(n) -i.
Since u is either x or s(x), we deduce that uθ is either k or k + 1. In the latter case, uθ > J(n) -i + 1. In the former case, l u ∨ D is of depth 0 by Proposition 4.6, and level(D) = m + 1 < i so that uθ = k = J(n) -m > J(n) -i + 1. Therefore, in every case, uθ > J(n) -i + 1 ≥ I(n) -j -i + 1 which contradicts our assumption.

• Now assume that uθ > I(n) -i -j + 1. Since Dθ is the minimal instance of a clause in S| [⊥,i[ that is false in J and since S is saturated up to level i, we may assume that D θ ≺ l u θ. Indeed, every literal in D θ must be smaller or equal to l u θ, and if l u θ occurs in D θ then the factorization rule applied to D would generate a clause with a strictly smaller instance that is false in J (notice that this new clause is actually equivalent to D, thus it must be an element of S| [⊥,i] : it cannot be redundant, since in this case D would be also redundant). Literal l u cannot be positive because if this were the case, D would be of the form p u ∨ D ∨ D and by construction, p uθ would be interpreted to true in J and Dθ would be true in J. Therefore, l u is a negative literal ¬p u and J(p uθ ) = true. Thus, by construction,

S| [⊥,i[ contains a clause of the form E = p v ∨ E ∨ E
where E is parameter-free and E is purely equational, and there exists a substitution θ such that vθ = uθ and ∀l ∈ E , lθ ≺ p vθ , and

J |= s (E ∨ E )θ .
The resolution rule applied to D and E generates a clause of the form

F = (E ∨ E ∨ D ∨ D )σ,
where σ is the mgu of u and v. An instance of this clause is

F = E θ ∨ D θ ∨ E θ ∨ D θ,
which is strictly smaller than Dθ and is false in J. Since S is saturated up to level i, F is levelredundant in S, hence there exist clauses C 1 , . . . , C m ∈ S and substitutions σ 1 , . . . , σ m such that

C 1 σ 1 , . . . , C m σ m F and C 1 σ 1 , . . . , C m σ m |= s F
. By Lemma 4.14, F is of level at most i, hence so are C 1 , . . . , C m . For all j = 1, . . . , m, if C j is of level i, then J |= s C j σ j by the first case above (i.e. the case D ∈ S| i ), and if the level of C j is strictly less than i, then since C j σ j F ≺ Dθ, the minimality condition on Dθ entails again that J |= s C j σ j . Therefore, in all cases, J |= s F , which is impossible.

In practice, Lemma 6.6 by itself is not sufficient to define a suitable loop detection rule, indeed, Condition 2 is difficult to check and Condition 3 is too restrictive. We now exhibit sufficient conditions guaranteeing the existence of a loop in a derivation. The first one tackles Condition 2. It turns out that this condition is always satisfied if we assume that S is generated by resolution from a set of clauses whose levels are lower than i. Intuitively, this condition states that the clauses in S are not arbitrary: they must be obtained by applying inference rules from a clause set whose level is bounded (by k). In particular, the set of all clauses obtained by resolution from a k-normalized set of clauses is obviously k-reducible: it suffices to take for S the initial set of clauses. Lemma 6.8. Let S be a k-reducible set of normalized clauses. For every

i ≥ k, S| i ∪ S| ⊥ |= s S| i+1 ; hence S| i ∪ S| ⊥ |= s S| [i,∞[ .
Proof: Since S is k-reducible, there exists a k-normalized set of clauses S such that every clause C in S of level i + 1 is derivable from S , and every clause in the derivation is level-redundant w.r.t. S. We prove by induction on the length of the derivation that for every clause C of level i + 1 occurring in this derivation, S| i ∪ S| ⊥ |= s C . Since S is k-normalized and C is of level i + 1 > k, the length of the derivation is greater than 0. We assume C is deduced by resolution from level-redundant parent clauses D 1 , D 2 , the case where C is generated by the factorization rule is similar. By Lemma 4.14, D 1 and D 2 can be of levels ⊥,

i or i + 1. If D 1 is of level ⊥ or i, then S| i ∪ S| ⊥ |= s D 1 by Proposition 6.2.
Otherwise by the induction hypothesis, S| i ∪S| ⊥ |= s D 1 . The same property holds for D 2 ; consequently, the parents of C are logical consequences of

S| i ∪ S| ⊥ , hence S| i ∪ S| ⊥ |= s C . Since S| i ∪ S| ⊥ |= s S| i+1 , we also have S| i ∪ S| ⊥ |= s S| i+1 ∪ S| ⊥ ,

and a straightforward induction proves that for all

j ≥ i, S| i ∪ S| ⊥ |= s S| j . Since S| [i,∞[ def = j≥i S| j ,
the second part of the lemma also holds.

We now show how ground clauses can basically be discarded altogether to ensure that Condition 3 of Lemma 6.6 holds. Definition 6.9. For all i > 0, we denote by S| i the set of non-ground clauses of level i in S.

Note that, by definition of a normalized clause, every ground clause of S| i has the form n ≈ s i-1 (0) ∨ C where C contains only literals of index 0. Lemma 6.10. Let S be a k-reducible set of normalized clauses.

If i > k, then S| i ∪ S| ⊥ |= s S| i .
Proof: Let C ∈ S| i . Since S is k-reducible, by definition there exists a derivation of C from a set of k-normalized clauses, and every clause in this derivation is level-redundant w.r.t. S. We prove by induction on the length of the derivation that for every clause C of level i occurring in the derivation, S| i ∪ S| ⊥ |= s C (taking C = C then enables to conclude). This is obvious if C is not ground. If C is ground, then since i > k, the length of the derivation is greater than 0. We assume C was deduced from two clauses D 1 and D 2 by resolution (the case where C was deduced by factorization is similar), and by Lemma 4.14, D 1 and D 2 are of level i or ⊥. By the induction hypothesis,

S| i ∪ S| ⊥ |= s D 1 , D 2 |= s C .
Proposition 6.11. Let S be a set of clauses and let C be a clause of a level i, such that

C l S. If C is not ground then C l S| ⊥ ∪ S| i .
Proof: By definition there exist m clauses C 1 , . . . , C m in S, of levels ⊥ or i such that for every ground substitution σ there exist m ground substitutions θ 1 , . . . , θ m such that Cθ 1 , . . . , Cθ m |= s Cσ and C 1 θ 1 , . . . , C m θ m Cσ. Furthermore, since C is not ground, by the definition of level-redundancy, C 1 , . . . , C m are not ground. For i = 1, . . . , m, if C i is of level ⊥ then it occurs in S| ⊥ and if it is of level i, then, since it is not ground, it occurs in

S| i . Thus C 1 , . . . , C m ∈ S| ⊥ ∪ S| i and C l S| ⊥ ∪ S| i .
Thanks to the results above, we can define a set of pruning clauses, all of which are compatible with the considered set of clauses. Definition 6.12. Let S be a k-reducible set of clauses. We denote by Pr(S) the set of pruning clauses of the form n < i + j such that: 2. S is saturated up to level i.

3. S| i+j = shift(S| i , j) (up to a renaming of variables). Theorem 6.13. Let S be a k-reducible set of normalized clauses. Any clause in Pr(S) is compatible with S.

Proof: Let i, j be natural numbers satisfying the conditions of Definition 6.12. It is clear that if S ∪ {n < i + j} is s-satisfiable then so is S, we now prove the other implication and assume that S is s-satisfiable.

Let T = S| [⊥,i[ ∪ l≥i S| l . By definition, T | l = S| l if l < i, and T | l = S| l if l ≥ i. Furthermore, since S is k-reducible,
so is T which is also normalized, and by Lemma 6.10, S is equivalent to T . Hence it suffices to show that T ∪ {n < i + j} is s-satisfiable. We prove that T satisfies the application conditions of Lemma 6.6.

1. T is saturated up to level i. Let C be a clause deduced from clauses in T | [⊥,i[ = S| [⊥,i[ . Since S
is saturated up to level i, C is level-redundant with respect to S, i.e., C l S. If the level of C is strictly less than i, then we deduce that C l S| [⊥,i[ , hence C l T . Otherwise, by Lemma 4.14, C cannot be ground, thus C l S| ⊥ ∪ S| i by Proposition 6.11.

T |

i ∪ T | ⊥ |= s T | [i,∞[
. This is a direct application of Lemma 6.8.

3.

T | i contains no ground clause. This is obviously the case by definition of S| i .

4. j = 0. This is the case by hypothesis.

T |

⊥ ∪ T | i+j |= s shift(T | i , j)
. By hypothesis, S| i+j = shift(S| i , j) and by construction,

S| ⊥ ∪ S| i+j = T | ⊥ ∪T | i+j . Thus T | ⊥ ∪T | i+j |= s shift(S| i , j). Since S| i = T | i , we have shift(S| i , j) = shift(T | i , j), hence the result.
Note that Conditions 2 and 3 in Definition 6.12 can be tested in polynomial time w.r.t. the size of the clause sets. Theorem 6.13 only applies to k-reducible clause sets. However, this is not really restrictive because, as we shall see, any clause set generated from a finite set of normalized clauses S by the resolution calculus must be k-reducible, where k is the maximal level of the clauses in S (see Lemma 7.3 for details). Example 6.14. Consider the clause set S = {1, . . . , 8} in Example 3.5 (generated from the formula p n ∧ (∀x p s(x) ⇒ p x ) ∧ ¬p 0 ):

1 n ≈ x ∨ p x (level 1) 2 p y ∨ ¬p s(y) (level ⊥) 3 ¬p 0 (level ⊥) 4 n ≈ s(y) ∨ p y (resolution, 1,2) (level 2) 5 n ≈ 0 (resolution, 1,3) (level 1) 6 n ≈ s(0) (resolution, 4,3) (level 2) 7 n ≈ s(s(y)) ∨ p y (resolution, 2,4) (level 3) 8 n ≈ s(s(0)) (resolution, 7 ,3) (level 3)
The initial clauses 1, 2, 3 are of level ⊥, 0 or 1, thus S is 1-reducible. Let i = 2 and j = 1, then S| i = {n ≈ s(y) ∨ p y } and S| i+j = {n ≈ s(s(y)) ∨ p y } (clauses 6 and 8 are dismissed since they are ground, according to Definition 6.9). Thus shift(S| i , j) = {n ≈ s(s(y)) ∨ p y } = S| i+j , and Condition 3 of Definition 6.12 trivially holds. Furthermore, it is straightforward to check that S is saturated up to level i.

Hence the pruning clause n ≈ s(s(s(x))), i.e. n < 3, occurs in Pr(S), hence can be added to S. Together with clauses 5, 6 and 8, we obtain a finite and purely equational clause set, whose unsatisfiability can be tested by standard algorithms. In this particular case, the obtained clause set is:

{n ≈ 0, n ≈ s(0), n ≈ s(s(0)), n ≈ s(s(s(x)))}, which is equivalent to n ≈ 0 ∧ n ≈ 1 ∧ n ≈ 2 ∧ n < 3. Therefore the initial clause set is s-unsatisfiable.
Example 6.15. Consider the following schema:

p 0 ∧ n x=0 (p x ⇒ q x ) ∧ n x=0 (q x ⇔ ¬q s(x) ) ∧ ¬q n ∧ ¬q s(n)
This schema can be encoded by the following clause set (see Section 5 for details):

1 p 0 (level ⊥) 2 ¬p x ∨ q x (level ⊥) 3 ¬q x ∨ ¬q s(x) (level ⊥) 4 q x ∨ q s(x) (level ⊥) 5 n ≈ x ∨ ¬q x (level 1) 6 n ≈ x ∨ ¬q s(x) (level 0)
We apply the calculus (assuming that p ≺ q):

7 q 0 (resolution 1,2) (level ⊥) 8 n ≈ 0 (resolution 7, 5) (level 1) 9 n ≈ s(x) ∨ q x (resolution 5,4) (level 2) 10 ¬p s(x) ∨ ¬q x (resolution 2, 3) (level ⊥) 11 n ≈ s(s(x)) ∨ ¬q x (resolution 9, 3) (level 3) 12 n ≈ s(s(0)) (resolution 11, 7) (level 3) 13 n ≈ s(s(s(x))) ∨ q x (resolution 11, 4) (level 4) 14 n ≈ x ∨ q x (resolution 4, 6) (level 1) 15 n ≈ s(x) ∨ ¬q x (resolution 3, 14) (level 2) 16 n ≈ s(0) (resolution 7, 15) (level 2) 17 n ≈ s(s(x)) ∨ q x (resolution 4, 15) (level 3) 18 n ≈ s(s(s(x))) ∨ ¬q x (resolution 17, 3) (level 4) 19 n ≈ s(s(s(0))) (resolution 18, 7) ( level 4)
Let i = 2, j = 2, and let S = {1-18}. S is saturated up to level 2. We have S | 2 = {9, 15}, S | 4 = {13, 18}, thus shift(S| 2 , 2) = S| 4 . The pruning rule applies and generates: n ≈ s(s(s(s(x))))

i.e. n < 4. Together with clauses 8, 10, 12 and 19, this yields a finite, purely equational, s-unsatisfiable, clause set.

Termination

In this section we define a pruning rule based on Theorem 6.13 and we show that the addition of this rule makes the calculus terminating, provided the rules are applied in a fair way.

The notion of level-redundancy is useful only to apply the pruning rule (Condition 2 in Definition 6.12 requires the clause set to be partially saturated up to level-redundancy). Once a pruning clause has been generated, the more general and standard notion of redundancy can be used instead. This yields the following: Definition 7.1. A clause C is deletable in a clause set S if and only if C is level-redundant in S or if C is redundant in S and S contains a pruning clause.

In order to take deletable clauses into account, we define derivations as sequences of clause sets: Definition 7.2. A pruning derivation from a clause set S is a (possibly infinite) sequence of clause sets (S i ) i∈I , with I = [0, n] or I = N, such that S 0 = S and for every i ∈ I \ {0}, one of the following conditions holds:

• S i = S i-1 ∪ {C}, where C ∈ Res(S i-1 ) (deduction step).

• S i = S i-1 ∪ {C}, where C ∈ Pr(S i-1 ) (pruning step).

• S i = S i-1 \ {C}, where C is deletable in S i-1 \ {C} (deletion step).

We write S p C if there exists a pruning derivation S 1 , . . . , S n from S such that C ∈ S n . The limit of a pruning derivation is the set of clauses S ∞ defined by: S ∞ def = i∈I S i .

In practice identifying all level-redundant or redundant clauses is unfeasible, thus only the clauses that are valid or subsumed are deleted. This fact has been taken into account for the termination proofactually the only form of redundancy testing that is needed is the deletion of valid clauses and subsumption by pruning clauses, which is sufficient to ensure that the level of the generated clause is bounded.

A derivation (S i ) i∈I is non-redundant if and only if the deletion steps are applied with the highest priority and if the deduction and pruning step are applied only if C is not deletable in S i-1 . It is fair if and only if for every level l there exists an i ∈ I such that all the clauses deducible from S i | [⊥,l] are deletable in S i (this may be enforced, for instance, by applying the inference rules with the highest priority on clauses of lower levels). Lemma 7.3. Let (S i ) i∈I be a pruning derivation from a k-normalized clause set, and assume the S i 's (i ∈ I) contain no pruning clause. Then for every i ∈ I, S i is k-reducible.

Proof: By definition every clause C in S i can be deduced from clauses in S. Thus there exists a derivation C 1 , . . . , C n from S such that C n = C. By definition, for every clause C j (1 ≤ j ≤ n), either C j ∈ S i , or C j was deleted by a previous deletion step. In both cases C j must be level-redundant with respect to S i (note that it is necessarily level-redundant and not just redundant, because the S i 's contain no pruning clause). Assume that S i-1 contains a pruning clause n ≈ s k (x). Then C is redundant w.r.t. S i-1 . All the clauses occurring in S i-1 but not in S i must be deletable in S i-1 , hence redundant w.r.t. S i-1 . By Proposition 7.4, C is redundant w.r.t. S i . If S i contains a pruning clause then the proof is completed, since C is deletable in S i . Otherwise, by definition, a deletion step must be applied on n ≈ s k (x), thus this clause is redundant w.r.t. S i-1 . Then S i-1 contains m clauses D 1 , . . . , D m (distinct from n ≈ s k (x)) and m substitutions θ j such that, in particular, D j θ j n ≈ s k (t), where t is any ground term of size greater than any term occurring in D j . By definition of the ordering (since equational literals are not comparable) we must have D j θ j = or D j θ j = n ≈ s k (x). If ∈ S i then C is level-redundant in S i hence the proof is completed. Otherwise, since t does not occur in D j , D j cannot be ground, hence D j must be of the form n ≈ s l (x), hence must be a pruning clause, which contradicts our assumption. Proposition 7.6. Let (S j ) j∈I be a non-redundant pruning derivation from a finite set of clauses. If I is infinite then so is S ∞ .

Proof: If S ∞ is finite and I is infinite, there exists i ∈ I such that no "new" clauses are generated after step i, i.e. such that for every clause C ∈ S ∞ , C occurs in S j for some j ≤ i. Then C must be deletable in S j , and by Corollary 7.5 every clause C ∈ S ∞ must be deletable in every set S k for k ≥ i. But then, since the derivation is non-redundant, no deduction and pruning can occur after step i (since the addition of deletable clauses is forbidden). Since the initial clause set is finite, there can be only finitely many deletion steps. Thus, I must be finite. Proposition 7.7. Consider a non-redundant pruning derivation (S i ) i∈I from a finite clause set.

1. If there exists an i ∈ I such that S i contains a pruning clause n ≈ s l (x), then any clause of a level at least l is deletable in S i .

2. If S ∞ contains a pruning clause, then I is finite.

Proof: We prove successively the two items.

1. Item 1 is a consequence of the fact that any normalized clause of level k ≥ l is of the form n ≈ s k+1-ε (x) ∨ D , where ε ∈ {0, 1}, and such a clause is obviously deletable.

2. If S ∞ contains a pruning clause n ≈ s l (x), then n ≈ s l (x) occurs in S i for some i ∈ I and by Item 1 all clauses of level greater than l + 1 are deletable in S i . By Corollary 7.5, these clauses are also deletable in every clause set S j for j ≥ i. Then, since (S j ) j∈I is non-redundant, the deduction and pruning steps after i cannot add any clause of a level greater than l + 1 by Item 1, and since there are only finitely many clauses of level at most l (up to renaming), Item 2 holds.

Theorem 7.8. If (S j ) j∈I is a fair, non-redundant pruning derivation from a finite and k-normalized clause set, then I is finite.

Proof: Assume I is not finite, then S ∞ cannot contain , and by Proposition 7.7 (2), S ∞ cannot contain any pruning clause either. Thus, by Lemma 7.3, S j is k-reducible for every j ∈ I. By Proposition 7.6, S ∞ is infinite (since I is infinite), and by Proposition 4.12, S ∞ must contain clauses of arbitrary levels, and this implies that for all levels i ∈ N, there exists a derivation step γ(i) such that every clause generated after this step is of a level strictly greater than i.

Still by Proposition 4.12, there are at most M = 2 4|Ω|+1 clauses of any given level, up to a renaming and the duplication of literals; there are therefore at most 2 M distinct normalized clause sets of the same level. We consider the integer l = 2 M + k + 1 and the set of clauses S γ(l) in the derivation, after which all generated clauses are of a level strictly greater than l. For all m ≤ l, let S m = {C idx | C ∈ S γ(l) | m }; by the pigeonhole principle, there exist i, j ∈ N such that k < i ≤ l, j = 0 and S i = S i+j . This implies that S γ(l) | i+j = shift(S γ(l) | i , j).

Since the derivation is fair by hypothesis and no clause of level i or i + 1 can be generated after step γ(l), the set S γ(l) is saturated up to level i. Therefore, the conditions of Theorem 6.13 hold, and the clause n < i + j occurs in Pr(S γ(l) ). It is also generable from all subsequent clause sets in the derivation, thus by the fairness hypothesis, the pruning step is applied at some point in the derivation, hence S ∞ contains a pruning clause, which contradicts our initial assumption.

From the previous termination proof, it is easy to obtain an upper bound on the time complexity of the algorithm. At most 2 2 4|Ω|+1 clause sets of size at most 2 4|Ω|+1 can be generated, thus since the rules can be applied in polynomial time w.r.t. the size of the clause set, the algorithm is at most doubly exponential. This is worse than the complexity of the tableaux-based proof procedure described in [START_REF] Aravantinos | A DPLL Proof Procedure for Propositional Iterated Schemata[END_REF] which is only simply exponential, in the case -which is the most analogous to the present paper-where the index variable can only be increased by 1 (the propositional schemata considered in [START_REF] Aravantinos | A DPLL Proof Procedure for Propositional Iterated Schemata[END_REF] possibly contain indices of the form i + k, where k can be strictly greater than 1; in the case in which k is not bounded by the size of the formula, the complexity of the procedure is then also doubly exponential). Intuitively, this is due to the fact that the nodes in the tableaux are labeled by sets of literals, instead of sets of clauses.

Extension to first-order logic without equality

Let Σ be a set of function symbols distinct from 0 and s, let V 1 be a set of first-order variables disjoint from V and let Ω 1 be a set of predicate symbols. Each symbol f in Σ ∪ Ω 1 is mapped to a unique natural number, called the arity of f .

The set of first-order terms is built as usual on the signature Σ and on the set of variables V 1 . A first-order clause is simply a clause, except that propositional variables are not elements of P anymore but have the form p(t 1 , . . . , t n ), where p is a predicate symbol of arity n and t 1 , . . . , t n are first-order terms. For example ¬p(a, f (u)) s(x) ∨p(f (v), b) x is a first-order clause. Note that p cannot be the equality predicate ≈, that has a special meaning, namely equality between parameters and natural numbers. Since we use the resolution calculus in this paper, the usual semantic equality between standard terms must be encoded by adding equality axioms.

A first-order substitution is a mapping from V 1 to the set of first-order terms. As usual, the applicability of a substitution σ can be extended to any expression e and the image of e is denoted by eσ. The notions of domain, ground substitution, unifier etc. are defined as in Section 2.

Note that the sets of first-order terms and index terms are disjoint: for instance, p(y) x is a first-order clause but p(x) x or p(0) x are not.

We denote by C↓ the set of clauses of the form Cσ where σ is a ground first-order substitution whose domain contains all the first-order variables in C (index variables are not instantiated). We also define S↓ def = C∈S C↓. The notion of the level of a first-order clause is a straightforward extension of the one for propositional clauses; in particular, the depths of the first-order terms occurring in a clause C are not taken into account when computing level(C). The notation shift(S, i) is defined in the same way. Proof: This is immediate since if a clause C is of level l then obviously any instance Cσ of C (where σ is a first-order substitution) is also of level l: indeed, the level of a clause C does not depend on the propositional variables, but only on the equational part of C and on the indices occurring in C, which by definition are not affected by σ.

The following fact is straightforward, since the shift operation does not affect non-equational literals: Proposition 8.2. For any first-order clause set S and for any i ∈ N, (shift(S, i))↓ = shift((S↓), i).

The semantics of sets of first-order clauses are defined in a usual way, by interpreting a set S as the set of its ground instances (thus clause sets are interpreted on the Herbrand domain). This definition is obviously not restrictive, since it is well-known that any satisfiable set of first-order clause has a Herbrand model. It is clear that S↓ can be considered as a set of propositional clauses: we can just take for the set of propositional variables Ω the set of all ground atoms p(t 1 , . . . , t n ). Then for any s-interpretation I we define: I |= s S if and only if I |= s S↓.

As usual, we assume the selection function sel is extended to first-order clauses in such a way that for every clause l ∨ C and for every substitution θ, if a literal lθ is selected in (l ∨ C)θ then l is also selected in l ∨ C. The inference rules for first-order clauses are depicted in Figure 2. We denote by Res(S) the set of clauses C that are deducible from S in one step. Note that the rules coincide with those of Figure 1 if the clauses are ground, which explains why we use the same notation Res(S).

p( t) u ∨ p( s) v ∨ C (p( t) u ∨ C)σθ ¬p( t) u ∨ ¬p( s) v ∨ C (¬p( t) u ∨ C)σθ
where: The notions of redundancy and level-redundancy can be extended to first-order clauses: C is redundant (resp. level-redundant) w.r.t. S if and only if every clause in C↓ is redundant (resp. level-redundant) w.r.t. S↓. The ordering ≺ on the elements of Ω (i.e. on the set of ground atoms p(t 1 , . . . , t n )) can be chosen arbitrarily and it is extended to indexed propositions (i.e. to atoms of the form p(t 1 , . . . , t n ) i ) as in Section 3. The notion of saturation up to a certain level is the same as in the propositional case. Then Pr(S) is defined as in Definition 6.12 and the notion of a pruning derivation can be extended as well. The following proposition relates as usual this "lifted" calculus to its ground version (including the pruning rule): Lemma 8.3. Let S be a normalized set of first-order clauses.

σ = mgu(u, v), θ = mgu( t, s) and p( t) u σθ is selected in (p( t) u ∨ p( s) v ∨ C)σθ or ¬p( t) u σθ is selected in (¬p( t) u ∨ ¬p( s) v ∨ C)σθ.
• Res(S↓) = (Res(S))↓.

• If C ∈ Pr(S) then C ∈ Pr(S↓).

Proof: The first item is standard (see for instance [START_REF] Leitsch | The resolution calculus[END_REF]) hence the proof is omitted. For the second item, consider a pruning clause of the form n < i + j such that S, i and j satisfy the conditions of Definition 6.12. Then, by Condition 2 in Definition 6.12, S is saturated up to level i, i.e., Res(S| [⊥,i[ ) l S, thus Res(S| [⊥,i[ )↓ l S↓. By the first item we get Res((S| [⊥,i[ )↓) l S↓, and by Proposition 8.1, Res((S↓)| [⊥,i[ ) l S↓, which means that S↓ is saturated up to level i. Furthermore, by Condition 3 of Definition 6.12, S| i+j = shift(S| i , j), thus S| i+j ↓ = shift(S| i , j)↓. By Proposition 8.2, we deduce S| i+j ↓ = shift(S| i ↓, j) and by Proposition 8.1, S↓| i+j = shift(S↓| i , j). Thus S↓, i and j satisfy the conditions of Definition 6.12, and n < i + j ∈ Pr(S↓).

As in the propositional case, we write S p C if there exists a pruning derivation S 1 , . . . , S n from S such that C ∈ S n . As already mentioned, Theorem 8.5 does not entail semi-decidability because S may be infinite. Of course, termination cannot be ensured for first-order clauses even if S is s-unsatisfiable and Theorem 7.8 does not hold for first-order clauses, since there may be infinitely many clauses of a given level.

Example 8.6. Let S be the following clause set:

1
p(y, z, cons(y, v)) s(x) ∨ ¬p(z, y, v) x 2 p(y, z, nil) 0 3 q(cons(u, y), v) 0 ∨ ¬q(y, v) x 4 q(cons(u, nil), u) s(x) ∨ ¬r x 5 even s(x) ∨ even x 6 ¬even s(x) ∨ ¬even x 7 even 0 8 n ≈ x ∨ ¬even x 9 n ≈ x ∨ ¬p(a, b, u) x ∨ ¬q(u, a) x 10 r 0

The symbols a, b are constant symbols, y, z, u, v are first-order variables; p(y, z, u) x holds if u is a list of length x of the form y, z, y, z, y, . . . and q(u, v) x holds if u is a list of length x whose last element is v. The atom r x holds if x is 0. Clauses 8 and 9 state that n is odd and that there is no list u satisfying both p(a, b, u) n and q(u, a) n , which obviously contradicts the previous axioms. r n holds if and only if n = 0. The calculus yields: At this point the pruning rule is applied (with i = 2 and j = 2), yielding the clause n < 4. With the clauses 11, 16, 22, 29, this proves the unsatisfiability of the original clause set.

Conclusion

We have devised a resolution-based proof procedure capable of handling sets of propositional or firstorder clauses indexed by natural numbers, which can be used to encode schemata of formulae. In the propositional case, this procedure has been proven to be sound, refutationally complete and terminating. In the first-order case, the procedure is only sound: the satisfiability problem is not even semi-decidable.

Future work includes the implementation of the calculus and experimental comparison with the tableau-based prover described in [START_REF] Aravantinos | RegSTAB: a SAT-Solver for Propositional Schemata[END_REF] for propositional schemata. In Section 7, we have shown that the complexity of the resolution-based procedure is at most doubly exponential w.r.t. the size of the initial clause set, but we do not know whether this bound is tight or not. The tableaux-based procedure of [START_REF] Aravantinos | A Schemata Calculus For Propositional Logic[END_REF] is "only" simply exponential, but this does not necessarily imply that the resolution calculus will be less efficient in practice. From a theoretical point of view, the extension to the equality case should also be considered (using the superposition calculus [START_REF] Bachmair | Rewrite-based Equational Theorem Proving with Selection and Simplification[END_REF]).

A very natural direction of research is to extend the termination results of Section 7 to subclasses of first-order clauses. This may be done by restricting ourselves to syntactic subclasses for which the resolution calculus terminates (see, e.g., [START_REF] Fermüller | Resolution Methods for the Decision Problem[END_REF] for numerous examples of such classes). However, this is not as straightforward as one may think because termination is usually ensured thanks to some specific ordering restriction strategy. In general, there is no guarantee that these ordering restrictions will be compatible with the ones already considered in the present paper, which impose that the literals are ordered according to their indices. For instance, a seemingly natural idea is to extend the present work to schemata of ground clause sets with equality by using the superposition calculus instead of resolution. This would allow one to handle for instance clauses such as a i ≈ b i or a i ≈ f (b i ), where a, b denote indexed constant symbols. As is well-known, the superposition calculus always terminates on (nonindexed) ground clauses. However, if indexed clauses are considered, termination cannot be ensured, due to the fact that a term indexed by i + 1 must be always greater than a term indexed by i, even if the latter is actually less complex according to the usual ordering: for example the set {p(a i ), a i+1 ≈ f (a i )} entails an infinite number of distinct clauses, of the form p(f k (a i )) (k ∈ N), obtained by repeatedly replacing a i+1 by f (a i ). Note that these clauses are all of the same level. Thus the results in the present paper do not extend to ground clauses with equality. Actually the satisfiability problem turns out to be undecidable for schemata of ground clause sets with equality [START_REF] Aravantinos | Schemata of SMT problems[END_REF]. Similarly, our calculus does not terminate on the rather simple clause set {¬p x (f (y))∨p s(x) (y), n ≈ x∨¬p x (a)}, although it is monadic and obviously satisfiable, since the ordering conditions impose to resolve on the literal p s(x) (y) (which normally would be avoided by standard resolution strategies).

Another direction of research is to refine the loop detection rule in order to get rid of the saturation condition, which is difficult to enforce for sets of first-order clauses. This may be done by analyzing more precisely the search space in order to identify cycles in the proof tree. Rather than considering the clause set as a whole, one would then focus on the specific clauses that are relevant for proving the considered property. This line of research is currently under investigation.

Definition 2 . 1 .

 21 (Schematic interpretations) An s-interpretation I is a function mapping• every parameter to a ground term in T (i.e. a natural number) and• every ground indexed atom to a truth value true or false.An s-interpretation I validates:

σ

  = mgu(u, v), and p u σ and ¬p v σ are selected in (p u ∨ C)σ and (p v ∨ D)σ Factorization

Lemma 4 . 13 .

 413 If S is a set of normalized non-valid clauses then any non-valid clause in Res(S) is also normalized (modulo the factoring of the equational literals).

Definition 6 . 3 .Example 6 . 4 .

 6364 If S is a set of clauses and i is a natural number, shift(S, j) denotes the set of clauses of the form n ≈ s i+j (x) ∨ C, where x ∈ V and n ≈ s i (x) ∨ C ∈ S. Consider the clause set

  therefore, I |= s D θ. The indices occurring in D are either x or s(x), thus the indices occurring in D θ are either k or k + 1. Furthermore, D is of depth ε = 1 if an index k + 1 occurs in D θ, and otherwise, ε = 0. Hence, the maximal index that can occur in D θ is I(n) -i -j + 1. By definition, I and J coincide on the atoms p l such that l ≤ I(n) -i -j + 1. Thus J |= s D θ, which implies that J |= s Dθ, a contradiction. Now assume that D ∈ S| [⊥,i[ . W.l.o.g. we assume that Dθ is the least instance w.r.t. ≺ of a clause in S| [⊥,i[ such that J |= s Dθ.

Definition 6 . 7 .

 67 A set of clauses S is k-reducible if and only if there exists a k-normalized (see Definition 4.11) set of clauses S such that for every clause C ∈ S there exists a derivation C 1 , . . . , C n from S such that C n = C and C 1 , . . . , C n are level-redundant w.r.t. S.

Proposition 8 . 1 .

 81 For any first-order clause set S, (S| l )↓ = (S↓)| l .

  Resolution p( t) u ∨ C ¬p( s) v ∨ D (C ∨ D)σθ where: σ = mgu(u, v), θ = mgu( t, s) and p( t) u σθ and ¬p( s) v σθ are selected in (p( t) u ∨ C)σθ and (¬p( s) v ∨ D)σθ Factorization

Figure 2 .

 2 Figure 2. The resolution calculus (first-order clauses)

Proposition 8 . 4 .Theorem 8 . 5 .

 8485 For all sets of normalized first-order clauses S, if S p C then for every clause D ∈ C↓, we have S↓ p D. Furthermore, if S↓ p D then there exists a clause C such that S p C and D ∈ C↓.Proof: This follows from Lemma 8.3 by an immediate induction on the length of the derivation. For any set of normalized first-order clauses S, S is s-unsatisfiable if and only if there exists a (possibly infinite) s-unsatisfiable set of purely equational clauses S such that for all C ∈ S , S p C.Proof: Assume S is s-unsatisfiable. Then so is S↓ and by Theorem 3.4, there exists an s-unsatisfiable set of purely equational clauses S ⊆ S↓ such that for all D ∈ S , S↓ p D. By Proposition 8.4, for every clause D ∈ S there exists a clause C such that S C and D ∈ C↓. Since D is purely equational, so is C, hence C↓ = {C} (since C contains no non equational literal, it contains no first-order variables). Thus S p C.Conversely, assume that there exists an s-unsatisfiable set of purely equational clauses S such that for all C ∈ S , S p C. Then since C↓ = {C} we have by Proposition 8.4: S↓ p C. By Proposition 3.2 and Theorem 3.4 (stating the soundness of the resolution and pruning rules for propositional clauses), S↓ is s-unsatisfiable. Hence S is also s-unsatisfiable.

  • a ground atom n ≈ t if and only if I(n) = t; • a ground atom p t if and only if I(p t ) = true; • a ground literal ¬a if and only if I does not validate a; • a ground clause C if and only if I validates at least one literal in C; • a non-ground clause C if and only if for every ground substitution σ of domain var(C), I validates Cσ;

• a set of clauses S if and only if it validates every clause in S.

By definition, an s-interpretation I validates a clause n ≈ s i (x) if and only if I(n) < i. Thus the notation n < i can be used as a shorthand for the clause n ≈ s i (x). We write I |= s S if and only if I validates S (in which case I is called an s-model of S). If S, S are two sets of clauses, we write S |= s S if and only if for every s-interpretation I, we have I |= s S ⇒ I |= s S . A clause or set of clauses S is s-satisfiable if and only if S has an s-model and s-valid if and only if every s-interpretation is an s-model of S.

  and ¬p u σ is selected in (¬p u ∨¬p v ∨C)σ. ∈ S ∪ Res({C 1 , . . . , C i-1 }). We write S C if and only if there exists a derivation C 1 , . . . , C n from S such that C = C n . A derivation of a set of clauses S is a derivation containing every clause in S . For example ¬p s(0) ,¬p x ∨ p s(x) , ¬p 0 is a derivation of {¬p 0 } from {¬p s(0) , ¬p x ∨ p s(x) }. A clause C is redundant w.r.t. a clause set S, written C S, if and only if for every ground substitution σ of domain var(C), there exist D 1 , . . . , D k ∈ S and σ 1 , . . . , σ k such that D 1 σ 1 , . . . , D k σ k |= s Cσ and D 1 σ 1 , . . . , D k σ k Cσ. If S is a clause set, we write S S if and only if every clause in S is redundant w.r.t. S . A clause set S is saturated if and only if Res(S) S.

	Figure 1. The resolution calculus
	every i ∈ [1, k], C i

is redundant in S I . The proof that any factor of a clause in S I is redundant is similar.

  Assume w.l.o.g. that there exists a k ∈ [0, m] such that for every i ∈ [1, k], I |= s E eq i and for every i ∈ [k + 1, m], I |= s E eq i (in other words, the k clauses such that I |= s E eq i are assumed to be at the beginning of the sequence E 1 , . . . , E m ). |= s E 1 , . . . , E m , and J |= s C ∨ D ∨ C ∨ D . But by hypothesis I |= s C ∨ D , hence, J |= s C ∨ D.

			By construction,
	E idx k+1 , . . . , E idx m ∈ S I , we show that E idx k+1 , . . . , E idx m |= s C ∨ D and E idx k+1 , . . . , E idx m	C ∨ D.
	Let J be an s-interpretation satisfying E idx k+1 , . . . , E idx m , and consider the s-interpretation J defined
	as follows: J (n) construction, J |= s E eq def = I(n) for every ground term n and J (p t ) i , for every i ∈ [1, k], and J |= s E idx def = J(p t ) for every ground atom p t . By i , for every i ∈ [k + 1, m]. Therefore
	J Therefore, we have E idx k+1 , . . . , E idx m |= s C ∨ D. Since E 1 , . . . , E m C ∨ D ∨ C ∨ D and since index
	literals and equational literals are not comparable, necessarily, E idx k+1 , . . . , E idx m	C ∨ D. Consequently,
	C ∨ D

  ∞[ by Condition 2, and since S = S| [⊥,i] ∪ S| [i,∞[ by definition, necessarily, S| [⊥,i] |= s S. We show that J |= s S| [⊥,i] , thus contradicting the fact that J |= s S. Let D be a clause in S| [⊥,i] and θ be a ground substitution such that J |= s Dθ. By definition, θ is either empty (if D is ground) or of the form x → s k (0), where x is the unique variable in D. First assume that D is of level i, i.e., that D ∈ S| i . By Condition 5, S| ⊥ ∪ S| i+j |= s shift(S| i , j), and since S| ⊥ ∪ S| i+j ⊆ S and I |= s S, this implies that I |= s shift(S|

  Proposition 7.4. If C is redundant (resp. level-redundant) w.r.t. S then any clause D redundant (resp. level-redundant) w.r.t. S ∪ {C} is also redundant (resp. level-redundant) w.r.t. S. Proof: Let σ be a ground substitution of domain var(D). Since D is redundant w.r.t. S ∪ {C} there exist n clauses D 1 , . . . , D n ∈ S ∪ {C} and n substitutions σ 1 , . . . , σ n such that D 1 σ 1 , . . . , D n σ n |= s Cσ and D 1 σ 1 , . . . , D n σ n ≤ Cσ. Moreover, if D is level-redundant in S ∪ {C}, then the D 1 , . . . , D n are of level ⊥ or of the same level as D. Let i ∈ [1, n]. We define a set of ground clauses E i as follows. If D i ∈ S then E i def = {D i σ i }. Otherwise, by definition we must have D i = C, thus there exist m clauses C 1 , . . . , C m ∈ S and m substitutions θ 1 , . . . , θ m such that C 1 σ 1 , . . . , C m θ m |= s D i σ i and C 1 θ 1 , . . . , C m θ m ≤ D i σ i ≤ Cσ. Moreover, if C is level-redundant, then the C 1 , . . . , C m are of level ⊥ or of the same level as C. We define E i def = {C 1 θ 1 , . . . , C m θ m }. By construction, the clauses in n i=1 E i are ground instances of clauses in S, that are smaller than Cσ. Moreover, we have n i=1 E i |= s n i=1 {D i σ} |= s Cσ and if C and D are level-redundant in S and S ∪ {C} respectively, then every clause in n i=1 E i is of level ⊥ or of the same level as C. Corollary 7.5. Let (S j ) j∈I be a fair, non-redundant pruning derivation. If C is deletable in S j for some j ∈ I, then C is deletable in every set S i such that i ∈ I, i ≥ j. Proof: The proof is by induction on i-j. It is obvious if i = j. If i > j, then by the induction hypothesis C is deletable in S i-1 . Assume that S i-1 contains no pruning clause. Then C is level-redundant w.r.t. S i-1 , by definition of a deletable clause. All the clauses occurring in S i-1 but not in S i must be deletable in S i-1 , hence level-redundant w.r.t. S i-1 . By Proposition 7.4, C is level-redundant w.r.t. S i , hence C is deletable in S i .

  ∨ ¬p(b, a, v) x ∨ ¬q(v, a) x (res, 13, 3) 18 n ≈ s(s(x)) ∨ ¬even x (res, 12, 6) 19 n ≈ s(s(x)) ∨ ¬p(a, b, v) x ∨ ¬q(cons(u, v), a) s(x) (res, 17, 1) 20 n ≈ s(s(x)) ∨ ¬p(a, b, nil) x ∨ ¬r x

	11	n ≈ 0	(res, 7, 8)
	12	n ≈ s(x) ∨ even x	(res, 5, 8)
	13	n ≈ s(x) ∨ ¬p(b, a, v) x ∨ ¬q(cons(u, v), a) s(x)	(res, 9, 1)
	14	n ≈ s(x) ∨ ¬p(b, a, nil) x ∨ ¬r x	(res, 13, 4)
	15	n ≈ s(x) ∨ ¬r x	(res, 14, 2)
	16	n ≈ s(0)	(res, 15, 1)
	17	n ≈ s(x) (res, 19,4)
	21	n ≈ s(s(x)) ∨ ¬r x	(res, 20, 2)
	22	n ≈ s(s(0))	(res, 21, 10)
	23
				(res, 25, 3)
		28	n ≈ s(s(s(0))) ∨ ¬r x	(res, 26, 2)
		29	n ≈ s(s(s(0)))	(res, 28, 10)

n ≈ s(s(x)) ∨ ¬p(a, b, v) x ∨ ¬q(v, a) x (res, 19, 3) 24 n ≈ s(s(s(x))) ∨ even x (res, 18, 5) 25 n ≈ s(s(s(x))) ∨ ¬p(b, a, v) x ∨ ¬q(cons(u, v),

a) x (res, 23, 1) 26 n ≈ s(s(s(x))) ∨ ¬p(b, a, nil) x ∨ ¬r x (res, 25, 4) 27 n ≈ s(s(s(x))) ∨ ¬p(b, a, v) x ∨ ¬q(v, a) x

Otherwise a schema as simple as p 10 . . . 0 k times could not be encoded in linear size.

As we shall see, this is the case in practice, since, by Lemma

[START_REF] Aravantinos | A Decidable Class of Nested Iterated Schemata[END_REF].14, all the clauses in S| [i,∞[ are generated from those in S|i, if i is greater than the level of the initial clauses.

This work has been partly funded by the project ASAP of the French Agence Nationale de la Recherche (ANR-09-BLAN-0407-01).