Vincent Aravantinos

Mnacho Echenim

Nicolas Peltier

A Resolution Calculus for Propositional Schemata

Introduction

This report describes a resolution calculus handling families of propositional formulae. The calculus is proven to be sound, refutationally complete and terminating. The class of propositional schemata we consider is more or less equivalent to the class of regular schemata introduced in [START_REF] Aravantinos | A schemata calculus for propositional logic[END_REF] although the definitions differ. The core of the resolution calculus (namely the resolution and factoring rule and the encoding of arithmetic parameters) is close to the one of [START_REF] Horbach | Superposition for fixed domains[END_REF] (although we use a different presentation). The main originality of our approach is the loop detection rule ensuring termination and refutational completeness.

Preliminaries

Informally, the syntax and semantics of our logic are almost identical to 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 are 0, succ (natural numbers).

Let Ω be a set of unary predicate symbols, or (indexed) propositional variables. Let P and V be two disjoint sets of variables. The elements in P are the parameters, and the ones 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 denote natural numbers (meta-variables).

The set of (arithmetic) terms T is the least set satisfying V ⊆ T , 0 ∈ T and t ∈ T ⇒ succ(t) ∈ T . Notice that T does not contain the parameters. A term is ground iff it is of the form succ 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. If x is a variable and i is a natural number then x + i denotes the term succ i (x).

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 . It is ground if t is ground. Notice that parameters only occur in equational atoms. Atoms of the form n ≈ t (resp. p t ) are called equational atoms (resp. indexed atoms).

1

A literal is either an atom (positive literal) or the negation of an atom (negative literal). A clause is a finite set (or disjunction) of literals (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 and C in the sets (disjunctions) of equational literals (resp. indexed literals) in C. If S is a set of clauses then S in denotes the set of clauses {C in | C ∈ S}. A clause C is purely equational iff C in = ∅ and parameter-free iff 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(x) [1,n] depth(l i ) (by convention depth( ) def = 0). A substitution σ is a function mapping every index variable x to a term xσ ∈ T (notice that parameters cannot be mapped). 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 iff for every x ∈ dom(σ), xσ is ground. A renaming is an injective substitution σ such that xσ ∈ V for every x ∈ dom(σ). A σ is flat if for every x ∈ V, xσ ∈ V ∪ {0}.

def = 0 if x ∈ V, depth(0) = 0, depth(succ(t)) = 1 + depth(t), depth(¬p t ) def = depth(p t ) def = depth(t), depth(n ̸ ≈ t) def = depth(n ≈ t) def = depth(t) and depth( ∨ n i=1 l i ) def = max i∈
σ is a unifier of t 1 , . . . , t n iff 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 ). Notice that in our simple case, all terms are of the form succ i (t) where t ∈ {0} ∪ V. Then any unifier of succ i (t) and succ j (s) where t, s ∈ {0} ∪ V (if it exists) is necessarily either empty or of the form t → succ j-i (s) (if t ∈ V, t ̸ = s and j > i) or of the form s → succ i-j (t) (if t ∈ V, t ̸ = s and j < i).

An interpretation I is a function mapping:

• Every parameter to a ground term in T (i.e. a natural number).

• Every ground indexed atom to a truth value true or false.

An interpretation I validates:

• A ground atom n ≈ t iff I(n) = t.

• A ground atom p t iff I(p t ) = true.

• A ground literal ¬a iff I does not validate a.

• A ground clause C iff it validates at least one literal in C.

• A non ground clause C iff for every substitution σ of domain var(C), I validates Cσ.

• A set of clauses S iff it validates every clause in S.

We write I |= S iff I validates S (then I is called a model of S). If S, S ′ are two sets of clauses, we write S |= S ′ iff for every interpretation I, we have I |= S ⇒ I |= S ′ . By definition, an interpretation I validates a clause n ̸ ≈ succ i (x) iff I(n) < i. Thus the notation n < i is a shorthand for the clause n ̸ ≈ succ i (x).

Proposition 1

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 (beside the variables in ⃗

x i ) are 0, succ, ≈, ̸ ≈ and the parameters. Since 0, succ are non interpreted, {C 1 , . . . , C k } is satisfiable iff the formula ∃⃗ n.

∧ k i=1 ∀ ⃗ x i C i holds in the empty theory, where ⃗ n is the set of parameters in C 1 , . . . , C n . The satisfiability problem is well known to be decidable for such formulae (by the results in [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] or even [START_REF] Comon | Equational problems and disunification[END_REF]).

Remark 2 Notice that by definition, any clause of the form n ̸ ≈ u ∨ n ̸ ≈ v ∨ C such that u and v are not unifiable is valid. For instance, n ̸ ≈ succ(x) ∨ n ̸ ≈ x holds in any interpretation, since n cannot be equal to both succ(x) and x.

3 The Calculus

Definition

If u and v are two terms, we write u ▹ v iff v = succ i (u) for some i > 0. This ordering is extended into a pre-ordering on atoms as follows:

p u ▹ q v iff u ▹ v.
We assume that a total ordering ≺ is given on elements of Ω. ≺ is extended into an ordering on atoms as follows: a ≺ a ′ iff either a ▹ a ′ or there exists a term u such that a = p u , a ′ = q u and p ≺ q. By definition, the equational atoms are not comparable.

Notice that ≺ is stable by substitution, i.e. a ≺ a ′ ⇒ aσ ≺ a ′ σ, for every substitution σ. ▹ 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 in ̸ = ∅, either sel(C) is a nonempty set of ▹-maximal negative literals or sel(C) is the set of ≺-maximal literals in C in . Notice that by definition equational literals are never selected (thus

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

n ̸ ≈ succ(succ(x)) ∨ ¬p x ∨ ¬p succ(x) ∨ q succ(x) ∨ r succ(x) .
Assume that p ≺ q ≺ r. p succ(x) , q succ(x) and r succ(x) are ▹-maximal. r succ(x) is ≺-maximal. sel can contain the literals ¬p succ(x) or r succ(x) but neither ¬p x nor q succ(x) .

The Resolution calculus is defined, as usual, by the following rules (we externalize factorization for technical convenience).

p u ∨ C ¬p v ∨ D (C ∨ D)σ
If: σ = mgu(u, v), p u σ and ¬p v σ are selected.

p u ∨ p v ∨ C (p u ∨ C)σ ¬p u ∨ ¬p v ∨ C (¬p u ∨ C)σ If: σ = mgu(u, v), p u σ or ¬p u is selected.
We denote by R(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 clause C is redundant w.r.t. a clause set S (written C ⊑ S) iff for every ground substitution σ of domain var(C), there exist D 1 , . . . , D n ∈ S and σ 1 , . . . , σ n such that

D 1 σ 1 , . . . , D n σ n |= Cσ and D 1 σ 1 , . . . , D n σ n ≼ Cσ. If S is a clause set, we write S ⊑ S ′ iff every clause in S is redundant w.r.t. S ′ . A clause set S is saturated iff R(S) ⊑ S. A derivation from a clause set S is a sequence of clauses C 1 , . . . , C n such that for every i ∈ [1, n], C i ∈ S ∪ R({C 1 , . . . , C i-1 }). We write S ⊢ C iff there exists a derivation C 1 , . . . , C n from S such that C = C n .
A derivation of S is a derivation containing every clause in S. For instance p 0 , ¬p x ∨ p succ(x) , p succ(0) is a derivation of {p succ (0)} from {p 0 , ¬p x ∨ p succ(x) }.

The notion of refutation differs from the usual one: since no rule can be applied on the equational part of the clauses, these literals cannot be eliminated: Definition 3 A refutation of S is a derivation from S of a finite unsatisfiable set of purely equational clauses. ♢

Notice that the satisfiability of this set can be tested by Proposition 1.

Basic properties of the calculus

It is very easy to check that the above rules are sound, i.e. the conclusion are logical consequences of the premises.

Proposition 4 Let S be a set of clauses. S |= R(S).

Proof. Immediate.

We now prove a weak form of refutational completeness. We first notice that the calculus is obviously complete for parameter-free clause sets: Proposition 5 Let S be a saturated set of parameter-free clauses. If S is unsatisfiable then ∈ S.

Proof. When the clauses contain no equational literals, our Resolution calculus coincides with the usual one. Hence the result.

Theorem 6 Let S be a saturated set of clauses. If S is unsatisfiable then there exists an unsatisfiable set of purely equational clauses S ′ such that S ′ ⊆ S.

Proof. Let I be an interpretation of the parameters in S. Let S g be the set of ground instances of the clauses in S. Let S I be the set of clauses 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. If S I has a model J then obviously I ∪ J is a model of S. Thus S I is unsatisfiable. We now check that S I is saturated.

Since S is saturated, so is S g (since the notion of saturatedness only depends on ground instances). 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

n clauses E 1 , . . . , E n ∈ S g such that E 1 , . . . , E n |= C ∨ D ∨ C ′ ∨ D ′ and E 1 , . . . , E n ≺ C ∨ D ∨ C ′ ∨ D ′ . Assume w.l.o.g. that there is a k ∈ [0, n] such that for every i ∈ [1, k], I |= E eq
i and for every i ∈ [k + 1, n], I ̸ |= E eq i (i.e. the k clauses such that I |= E eq i are assumed to be at the beginning of the sequence E 1 , . . . , E n ). By definition, we have E in k+1 , . . . , E in n ∈ S I . We show that E in k+1 , . . . , E in n |= C ∨ D. Let J be an interpretation satisfying E in k+1 , . . . , E in n . Let J ′ be the interpretation defined as follows: J ′ (n) def = I(n) and J ′ (A) def = J(A) for every ground atom A. By definition, J ′ |= E eq i , for every

i ∈ [1, k] thus ∀i ∈ [1, k], J ′ |= E i . Moreover, since J |= E in i , for every i ∈ [k + 1, n] we also have ∀i ∈ [k + 1, n], J ′ |= E i . Therefore J ′ |= E 1 , . . . , E n , hence J ′ |= C ∨ D ∨ C ′ ∨ D ′ . But I ̸ |= C ′ ∨ D ′ , thus J |= C ∨ D.
Moreover, since E 1 , . . . , E n ≺ C ∨D∨C ′ ∨D ′ , we must have E in k+1 , . . . , E in n ≺ C ∨ D (since index literals and equational literals are not comparable). Consequently, C ∨ D is redundant in S I .

By the same reasoning we can prove that any factor of a clause in S I is redundant.

Thus R(S I ) ⊑ S I and S I is saturated. Thus by Proposition 5, ∈ S I . Consequently, S contains a purely equational clause C I that is false in I. This holds for every interpretation I, thus S contains a set of purely equational clauses S ′ such that for every interpretation I of the parameters in S ′ , I ̸ |= S ′ . This implies that S ′ is unsatisfiable. Theorem 6 does not imply semi-decidability because S ′ may well be infinite:

Example 7 Let S = {n ̸ ≈ x ∨ p x , p y ∨ ¬p succ(y) , ¬p 0 }. The reader can easily check that S is unsatisfiable and that our calculus generates an infinite number of purely equational clauses of the form n ̸ ≈ succ i (0):

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

Restricting the language

We restrict ourselves to a particular class of clause sets. This class is very convenient from a theoretical point of view and, as we shall see in Section 8, it is expressive enough for our purpose. We shall firstly assume that the clauses contain at most one variable (e.g. we discard clauses such as p x ∨ p y where x, y are distinct variables). Furthermore, the clauses containing a variable should not contain any ground term (i.e. no occurrence of 0). For instance, a clause such as p x ∨ q 0 is forbidden.

Definition 8 Let t ∈ {0} ∪ V. A clause C is a t-clause iff every atom occurring in it is of the form p succ i (t) for some i ∈ N. ♢

Next, we assume that the non equational part of the clause is of depth 0 or 1 (the depth of the equational part is arbitrary). Finally, we strongly restrict the form of the equational part of the clauses: Definition 9 A clause C is normalized iff there exists a term t ∈ V ∪ {0} such that the following conditions hold:

• C eq is either empty or of the form n ̸ ≈ succ k (t).

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

• If t = 0 then depth(C in ) = 0.
A set of clauses S is normalized iff the following conditions hold:

1. S contains at most one parameter (always denoted by n in the following)

2. Every clause in S is normalized. ♢ For instance p x ∨¬p succ(x) , n ̸ ≈ succ(succ(x))∨p x or n ̸ ≈ 0∨q 0 are normalized, but n ̸ ≈ 0 ∨ p succ(0) , n ̸ ≈ succ(x) ∨ ¬p 0 ∨ q x or p succ(succ(x)) are not.
Definition 10 The level of a normalized clause is an element of N∪{⊥}, defined as follows:

• If C eq = then the level of C is ⊥. • If C eq ̸ = then level(C) def = level(C eq ) -level(C in ) + 1. S| i denotes the set of clauses in S of level i (where i ∈ N ∪ {⊥}). If I is a subset of N ∪ {⊥}, S| I denotes the set of clauses whose levels are in I. ♢ For instance, the levels of n ̸ ≈ succ(0) ∨ p 0 , n ̸ ≈ succ(succ(x)) ∨ p succ(x) and n ̸ ≈ succ(x) ∨ p x are all equal to 2. For any parameter-free clause C, the level of n ̸ ≈ 0 ∨ C is 1, the one of n ̸ ≈ succ(0) ∨ C is 2, etc. (because C necessarily has depth 0 in this case). The level of n ̸ ≈ succ(succ(x)) ∨ p x is 3 (as the one of its instance n ̸ ≈ succ(succ(succ(x))) ∨ p succ(x) ), the one of n ̸ = succ(succ(x)) ∨ p succ(x) is 2.
Intuitively, a clause of level ⊥ expresses either some universal property such as ∀x ¬p x ∨ p succ(x) or a ground property, e.g. p 0 , p succ(0) etc. A clause of level distinct from ⊥ is of the form n ̸ ≈ succ k (t) ∨ C where the only indices occurring in C are t or succ(t). It can be viewed as an implication: n ≈ succ k (t) ⇒ C. If t = 0 then the clause states a ground property that must be true if n is equal to succ k (0). If t is a variable x, the clause expresses an assertion that must hold for the natural number x = nl, assuming that n ≥ l. This could be written n ≥ l ⇒ C{x → n -l} but of course this last formula is not a clause.

Remark 11 For any interpretation I, the level of a clause C (if distinct from ⊥) is always equal to I(n) + 1i, where i denotes the maximal index of the (only) ground instance of C that is relevant in I (this instance depends on the value of n).

For example, consider the clause

C : n ̸ ≈ succ(x) ∨ p x . The level of C is 2. The only ground instance of C that is relevant for the interpretation I = {n → k} is of the form n ̸ ≈ succ(succ k-1 (0)) ∨ p succ k-1 (0) (since n ̸ ≈ succ(x) is true in I if x ̸ = succ k-1 (0)) where the value of n is k + 1. We have 2 = k + 1 -(k -1).
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 [⊥, i] denotes the set {⊥} ∪ [0, i].
Proposition 12 For every l ∈ N ∪ {⊥}, the number of normalized clauses of level l (on a given finite signature) is finite (up to renaming and up to duplication of literals).

Proof. A normalized clause is of the form n ̸ ≈ t ∨ C or C where C is a t-clause of depth 0 or 1. Furthermore, if t is fixed and if Ω is finite, the number of distinct t-clauses of depth 0 or 1 is finite (up to duplication of literals), since every literal in C is of the form p t , ¬p t , p succ(t) or ¬p succ(t) , for some p ∈ Ω.

Definition 13 A set of clauses is k-normalized if it is normalized and if the level of every clause in S is in [⊥, k].
♢ Section 8 gives hints on the expressive power of normalized clause sets.

The following propositions states straightforward properties of t-clauses:

Proposition 14 If C is a t-clause (where t ∈ V ∪ {0}) and if σ is flat then Cσ is a tσ-clause. Proposition 15 If C, D are two t-clauses then C ∨ D is a t-clause. Proposition 16 If C is a succ(t)-clause of depth 0 then C is a t-clause.
The next lemma states that the class of normalized clauses is preserved by the inference rules.

′′ i def = D eq i . Since S is normalized, there exists a term t i ∈ V ∪ {0} such that l i ui ∨ D ′ i is a t i -clause. Furthermore, D ′′ i is either empty or of the form n ̸ ≈ succ ki (t i ). Then C is of the form (D ′ 1 ∨ D ′ 2 ∨ D ′′ 1 ∨ D ′′ 2 )σ where σ = mgu(u 1 , u 2 ). By definition, u i is either t i or succ(t i ). Thus σ is of one of the following forms: ∅, {t 2 → t 1 }, {t 2 → succ(t 1 )} (with t 2 ∈ V and t 1 ∈ V ∪ {0}) or {t 1 → t 2 , t 1 → succ(t 2 )} (with t 1 ∈ V and t 2 ∈ V ∪ {0}).
Any atom occurring in D ′ i σ is of the form q tiσ or q succ(tiσ) . If σ is empty or of the form t 2 → t 1 or t 1 → t 2 then t 1 σ = t 2 σ (notice that if σ is empty then u 1 , u 2 are ground thus, since D 1 , D 2 are normalized we must have

u 1 = u 2 = t 1 = t 2 = 0). Since σ is flat, by Proposition 14, D ′ 1 σ is a t i σ-clause. By Proposition 15, D ′ 1 σ ∨ D ′ 2 σ is a t 1 σ-clause. D ′′ i is either empty or of the form n ̸ ≈ succ ki (t i ). Assume that D ′′ 1 and D ′′ 2 are not empty and that k 1 ̸ = k 2 . Then C contains the disjunction n ̸ ≈ succ k1 (t 1 σ) ∨ n ̸ ≈ succ k2 (t 2 σ). Since t 1 σ = t 2 σ and k 1 ̸ = k 2 , succ k1 (t 1 σ) and succ k2 (t 2 σ) are not unifiable, hence C is valid. Otherwise, D ′′ 1 ∨ D ′′ 2 is either empty or of the form n ̸ ≈ succ k1 (t 1 σ). Thus C is normalized.
Assume that σ is t 2 → succ(t 1 ). If D ′ 2 σ contains a atom of the form q succ(t2) then we have p t2 ▹q succ(t2) thus by definition of the selection function, the literal ¬p t2 would not be selected, which is impossible. Hence every atom in

D ′ 2 σ is of the form q t2σ = q succ(t1) , hence D 2 σ ′ is a t 1 -clause. D ′ 1 σ is obviously a t 1 -clause (since σ is the identity on D ′ 1 ), thus by Proposition 15, D ′ 1 σ ∨ D ′ 2 σ is 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 ̸ ≈ succ k1 (t 1 σ) ∨ n ̸ ≈ succ k2 (t 2 σ). Since t 2 σ = succ(t 1 ) and k 1 ̸ = k 2 + 1, succ k1 (t 1 σ) and succ k2 (t 2 σ) are not unifiable, hence C is valid. Otherwise, D ′′ 1 ∨ D ′′ 2 is either empty or of the form n ̸ ≈ succ k2+1 (t 1 ). Thus C is normalized. The proof is similar if σ is t 1 → succ(t 2 ). Now assume that C is deduced by factorisation, from a clause p u ∨ p v ∨ C ′ (resp. ¬p u ∨ ¬p v ∨ C ′ )
. By definition, u and v are either ground or of the form succ i (x) and succ j (x) for some variable x. Since p u ∨p v ∨C ′ (resp. ¬p u ∨¬p v ∨C ′ ) is non valid, u and v must be unifiable. Thus we must have u = v hence the mgu of u and v is empty. Hence C = p u ∨C ′ (resp. C = ¬p u ∨C ′ ) is normalized. Factorisation cannot be applied in a non trivial way on normalized clauses (it simply removes a literal).

Lemma 18 relates the level of any clause to that of its parents.

Lemma 18 Let S be a set of normalized clauses. Let C be a non valid clause of level j ∈ N in R(S) deduced from two parent clauses D 1 , D 2 in S of level k 1 , k 2 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 .
Proof. By definition, there exists a term

t ∈ V ∪ {0} such that C is of the form n ̸ ≈ succ j-1+ϵ (t) ∨ C ′ and C ′ is a t-clause of depth ϵ (notice that j ̸ = ⊥ by hypothesis). Similarly, If D i is not parameter-free, then D i is of the form n ̸ ≈ succ ki-1+ϵi (t i ) ∨ D ′ i where D ′ i is a t ′ i -clause of depth ϵ i .
We must have succ j-1+ϵ (t) = succ ki-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. u 1 and u 2 are of the form 0, x i or succ(x i ) where x i is a variable, thus σ is either empty (if

u 1 = u 2 = 0) or of the form x 1 → 0 (if u 1 = x 1 and u 2 = 0) or x 2 → 0 (if u 1 = 0, u 2 = x 2 ) or x 1 → x 2 (if either u 1 = x 1 and u 2 = x 2 or u 1 = succ(x 1 ) or u 2 = succ(x 2 )) or x 1 → succ(x 2 ) (if u 1 = x 1 and u 2 = succ(x 2 )) or x 2 → succ(x 1 ) (if u 1 = succ(x 1
) and u 2 = x 2 ). Several cases must be distinguished according to the form of σ.

• If σ is empty then we must have u 1 = u 2 = 0. Then D 1 , D 2 are ground, hence C is also ground. Furthermore, if D i is not parameter-free, we have j -

1 + ϵ = k i -1 + ϵ i . By definition of normalized clauses we have ϵ = ϵ i = 0, thus j = k i . • If σ is of the form x 1 → x 2 or x 1 → 0 or x 2 → 0 then D in 1 and D in 2 must be of the same depth, thus ϵ 1 = ϵ 2 . If D i is not parameter-free, we have j -1 + ϵ = k i -1 + ϵ i , thus k i = j + ϵ -ϵ i . If ϵ = 1 then this means that C ′ is of depth 1. But every literal in C ′ occurs in D ′ j σ for some j = 1, 2, thus D ′ j σ is of depth 1 for some j = 1, 2. Since σ is flat, D j is of depth 1, hence ϵ j = 1. Since ϵ 1 = ϵ 2 we deduce that ϵ i = 1, hence ϵ -ϵ i ≤ 0 and k i ∈ {0, j, j -1}.
If C is ground then we must have u 1 = 0 or u 2 = 0, hence ϵ 1 = ϵ 2 = 0. Moreover, ϵ = 0 by definition of the notion of normalized clause. Thus k i = j.

Finally if D 1 and D 2 are both not parameter-free we remark that, since u 1 and u 2 are of same depth we must have

ϵ 1 = ϵ 2 hence k 1 = k 2 .
• If σ is of the form x 1 → succ(x 2 ) then u 1 = x 1 and u 2 = succ(x 2 ). In this case C is not ground. If D 1 is not parameter-free, we have j -

1 + ϵ = k 1 -1+ϵ 1 +1, thus k 1 = j+ϵ-ϵ 1 -1. Moreover we have ϵ 1 = 0 since u 1 = x 1 is maximal. Thus k 1 = j + ϵ -1 ∈ {j -1, j}. If D 2 is not parameter-free, we have j -1 + ϵ = k 2 -1 + ϵ 2 , thus k 2 = j + ϵ -ϵ 2 . Moreover we have ϵ 2 = 1 since u 2 = succ(x 2 ) occurs in D 2 . Thus k 2 = j -1 + ϵ ∈ {j -1, j}.
• The case where σ is of the form {x 2 → succ(x 1 )} is symmetric.

Loop Detection

In this section we refine the calculus proposed in Section 3 by defining a loop detection rule that is capable of pruning infinite derivations. . Since the set of x-clauses is finite there must exist, by the pigeonhole argument, two natural numbers i and j > 0 such that S i = S i+j . This means 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: indeed if S i = S i+j then n ̸ ≈ succ i+j (x)∨S i+j is equivalent to n ̸ ≈ succ i ∨S i , up to a shift n → n+j.

We shall show that, under some particular conditions, the existence of such a "cycle" in the derivation allows one to derive an upper bound on the value of the parameter n: if S is 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 one can obtain another model J such that J(n) = I(n)j by applying the translation n → nj on I. This implies that the clause n < i + j (written n ̸ ≈ succ i+j (x)) can be derived. Then it is easy to see that every clause of level strictly greater than i + j is redundant w.r.t. n < i + j (since n ̸ ≈ succ i+j (t) ∨ C is obviously subsumed by n ̸ ≈ succ i+j (x)). Consequently, once the pruning clause n < i + j has been generated, only finitely many non redundant clauses can be deduced.

Obviously, this result does not hold for any derivation: for instance if the initial clause set S contains clauses of arbitrary level, then the value of parameter must also be arbitrary. Now we give the formal definition of the conditions that must be satisfied by S. We start by slightly restricting the notion of redundancy:

1 to simplify the presentation we assume that every clause C ∈ S k is of depth 1.

Definition 19 A clause C is level-redundant w.r.t. S (written C ⊑ l S) iff for every ground substitution σ of domain var(C) there exist n clauses C 1 , . . . , C n such that:

• If C is non ground then C 1 , . . . , C n are non ground.

• C 1 , . . . , C n are either of level ⊥ or of the same level as C.

• There exist n substitutions θ 1 , . . . , θ n such that C 1 θ 1 , . . . , C n θ n |= Cσ and

C 1 θ 1 , . . . , C n θ n ≼ Cσ.
If S ′ is a set of clauses, we write S ′ ⊑ l S iff ∀C ∈ S, C ⊑ l S. ♢ For instance, p x is redundant w.r.t. {p 0 , p succ(x) } but not level-redundant (since p 0 is ground and

p x is not). n ̸ ≈ succ(x) ∨ p x is redundant w.r.t. {p x , ¬p x } but not level-redundant since level(n ̸ ≈ succ(x) ∨ p x ) = 2 and level(p x ) = level(¬p x ) = ⊥ < 2.
Notice that every tautological clause and every clause subsumed by a clause in S is level-redundant w.r.t. S, thus in practice these two notions coincide.

Definition 20 A set of clauses S is saturated up to level i iff R(S| [⊥,i[ ) ⊑ l S.♢ If S is a set of clauses and i is a natural number, shift(S, i) denotes the set of clauses of the form n ̸ ≈ succ i+j (x) ∨ C, where x ∈ V and n ̸ ≈ succ j (x) ∨ C ∈ S.
Example 21 Consider the clause set

S = {n ̸ ≈ succ(succ(x))∨¬p(x)∨p(succ(x)), n ̸ ≈ succ(x)∨q(x), n ̸ ≈ 0∨p(x), ¬r(x)}.
We have shift(S, 0) = {n ̸ ≈ succ(succ(x)) ∨ ¬p(x) ∨ p(succ(x)), n ̸ ≈ succ(x) ∨ q(x)}, shift(S, 1) = {n ̸ ≈ succ(succ(succ(x))) ∨ ¬p(x) ∨ p(succ(x)), n ̸ ≈ succ(succ(x)) ∨ q(x)}, shift(S, 2) = {n ̸ ≈ succ(succ(succ(succ(x)))) ∨ ¬p(x) ∨ p(succ(x)), n ̸ ≈ succ(succ(succ(x))) ∨ q(x)} etc. Notice that ¬r(x) or n ̸ ≈ 0 ∨ p(x) cannot occur in shift(S, i) because they contain no literal of the form n ̸ ≈ succ j (x), where x ∈ V. ♣ Lemma 22 will set the foundations for defining the loop detection rule. This lemma applies when we detect that the clauses of a certain level i in S are logically entailed by the ones of a level i + j > i, up to a shift on the parameter n. This means that any model of S| i+j is also a model of S| i , up to a shift n → nj. If, moreover, we assume that S is saturated up to level i, this implies as we shall see that for any model I of S such that I(n) ≥ i + j, one can construct a model J of S such that J(n) = I(n)j < I(n). To get a model of S| [i,∞[ , it suffices to apply the translation n → nj on the model I, namely to fix the truth values of the variables p i , p i+1 , p i+2 , . . . in J as the ones of p i+j , p i+j+1 , p i+j+2 , . . . in I; then, since S is saturated up to level i, it is possible to show that this interpretation can be extended into a model of S. Thus, satisfiability is preserved when we state that the value of n is strictly lower than i + j. As explained before, adding this assertion into S makes every clause of level greater than i + j redundant since it is subsumed by n < i + j.

Lemma 22 Let S be a set of normalized clauses of parameter n and let i, j be natural numbers satisfying the following conditions:

1. S is saturated up to level i.

S|

i ∪ S| ⊥ |= S| [i,∞[ 3. S| i contains no ground clause. 4. j ̸ = 0. 5. S| ⊥ ∪ S| i+j |= shift(S| i , j).
Then: S is satisfiable iff S ∪ {n < i + j} is.

Proof. Let I be an interpretation satisfying S. W.l.o.g. we assume that the value of n is minimal (w.r.t. the usual ordering on natural numbers), i.e. for every interpretation J such that J(n) < I(n) we have J ̸ |= S.

Assume that I ̸ |= {n < i + j} (i.e. I(n) ≥ i + j which implies that I(n) > 0 since j ̸ = 0 by assumption).

We construct an interpretation J as follows.

• J(n)

def = I(n) -j. By Condition 4 this implies that J(n) < I(n) thus J ̸ |= S.
• The value of the ground atom 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 + 1, then suppose J(q k ′ ) is already defined for every literal q k ′ lower than p k . Thus, for any clause made only of such literals, its value under J is completely defined. Notice also that the value of every purely equational clause only depends on J(n) and is thus also completely defined. Consequently, we can define J(p k ) as follows: if S| [⊥,i[ contains a clause which has an instance of the form p k ∨ C, where all indexed atoms of C are lower than p k and J ̸ |= C, then we set J(p k ) to true. Otherwise we set it to false.

Let S ′ = S| [⊥,i] . By Condition 2 we have S| i ∪ S| ⊥ |= S| [i,∞[ thus S ′ |= S (since by definition S = S| [⊥,i] ∪ S| [i,∞[ ).
We now show that J |= S ′ (thus contradicting the fact that J ̸ |= S).

Let D be a clause in S ′ and let θ be a ground substitution such that J ̸ |= Dθ. By definition θ is either empty (if D is ground) or of the form x → k where x is the unique variable in D.

First, assume that D ∈ S| i . By Condition 5 S| ⊥ ∪S| i+j |= shift(S| i , j). Since I |= S ⊇ S| ⊥ ∪ S| i+j this implies that I |= shift(S| i , j). By definition, D is of the form n ̸ ≈ succ i-1+ϵ (t) ∨ D ′ , where D ′ is a t-clause of depth ϵ. By condition 3 D is not ground, thus t is a variable x. Then shift(S| i , j) contains the clause

n ̸ ≈ succ i-1+ϵ+j (x) ∨ D ′ and I |= n ̸ ≈ succ i-1+ϵ+j (x) ∨ D ′ . Since J ̸ |= Dθ we must have J(n) = i -1 + ϵ + k. Thus I(n) = J(n) + j = i -1 + ϵ + k + j, hence (since I |= n ̸ ≈ succ i-1+ϵ+j (x)θ ∨ D ′ θ), we have I |= D ′ θ.
The indices occurring in D ′ are either x or succ(x). Thus the indices occurring in D ′ θ are either k or k + 1. Furthermore if an index k + 1 occurs in D ′ θ then D is of depth 1, thus ϵ = 1 (otherwise ϵ = 0). Hence the maximal index that can occur in D ′ is I(n)ij + 1. By definition of J, I and J coincide on the propositions p l such that l ≤ I(n)ij + 1. Thus we have J |= D ′ θ, hence J |= 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 ̸ |= Dθ. Note that D cannot be empty (otherwise S would be unsatisfiable). If D is purely equational then, since D cannot be valid, D must be of the form n ̸ ≈ succ l (t) for some l < i and t ∈ V ∪ {0} (since D ∈ S| [0,i[ and D is normalized). Then D is equivalent to either n < l (if t ∈ V) or n ̸ = l (if t = 0), where l < i. In the first case, we have I ̸ |= D which is impossible since I is a model of S and D ∈ S ′ ⊆ S. In the second case, since l < i and J(n

) = I(n) -j ≥ i we have J |= D.
Thus D contains at least one index literal. We denote by l u the maximal index literal in D (there is only one maximal index literal since D contains only one variable and since ≺ is total). D is of the form l u ∨ D ′ ∨ D ′′ , where D ′ is parameter-free, D ′′ is purely equational (with possibly D ′ , D ′′ = ), and for any literal l ∈ D ′ θ, l ≼ l u θ. By definition of the ordering, this implies that the index of every literal l ∈ D ′ θ is smaller or equal to uθ.

We distinguish two cases according to the value of uθ.

• If uθ ≤ I(n) -i -j + 1,
(n) = l + k for some k ∈ N (if t = x) or J(n) = l (if t = 0). Because D ′′ is not empty, we cannot have D ∈ S| ⊥ thus D ∈ S| [0,i[ , hence l < i.
Thus we cannot have J(n) = l (since by hypothesis I(n) > i + j and by definition of J, J(n) = I(n)j, thus J(n) ≥ i), hence we are in the first case and k > J(n)i. u is either x or succ(x). Thus uθ is either k or k + 1. Furthermore, if u is x then l u ∨ D ′ is an x-clause of depth 0 (otherwise l u would not be maximal), hence l + 1 < i and in this case we have k > J(n)-i+1. Thus in every case uθ ≥ J(n)-i+1 ≥ I(n)-j -i+1 which contradicts our assumption.

• Now assume that uθ > I(n)ij + 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 can assume that D ′ θ ≺ l u θ (indeed, every literal D ′ θ must be smaller than l u θ, furthermore, if l u θ occurs in D ′ θ then the factorization rule applies on D and generates a clause with a strictly smaller instance that is false in J). By definition of J this implies that l u is a negative literal ¬p u . But then since

J(p uθ ) = true, S| [⊥,i[ contains a clause of the form p v ∨ E ′ ∨ E ′′ such that E ′ is parameter-free, E ′′ is purely equational, there exists a substitution θ ′ such that vθ ′ = uθ, J ̸ |= (E ′ ∨ E ′′ )θ ′ and ∀l ∈ E ′ , lθ ′ ≺ p vθ ′ .
The resolution rule applies on D and p v ∨E ′ ∨E ′′ and yields a clause of the form (E ′ ∨ E ′′ ∨ D ′ ∨ D ′′ )σ, where σ is the mgu of u and v. An instance of this clause is

E ′′ θ ′ ∨ D ′′ θ ∨ E ′ θ ′ ∨ D ′ θ.
(E ′ ∨ E ′′ ∨ D ′ ∨ D ′′ )σ which is impossible.
Lemma 22 by itself is not sufficient to define a suitable loop detection rule. Indeed, Condition 2 is hard to check and Condition 3 is not guaranteed. Fortunately, we show that these two conditions always hold for set of clauses that are obtained from a k-normalized clause set:

Definition 23 A set of clauses S is k-reducible iff there exists a k-normalized 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. ♢

Lemma 24 Let S be a k-reducible set of normalized clauses. For every i ≥ k,

S| i ∪ S| ⊥ |= S| i+1 . Hence S| i ∪ S| ⊥ |= S| [i,∞[ .
Proof. Since S is k-reducible, there exists a k-normalized set of clauses S ′ such that C is derivable from S ′ . Furthermore, every clause in the derivation is level-redundant w.r.t. S.

We show, by induction on the length of the derivation that for every clause C ′ of level i + 1 occurring in this derivation, we have S| i ∪ S| ⊥ |= C ′ . Since C ′ is of level i + 1 > k, the length of the derivation is greater than 0. C ′ is deduced from two clauses D 1 , D 2 (resp. from a unique clause D 1 ) by resolution (resp. factorization). By Lemma 18, D 1 , D 2 (resp. D 1 ) are either in S| ⊥ or of level i or

i + 1. If D 1 is of level i or ⊥ then S| i ∪ S| ⊥ |= D 1 since D 1 is level-redundant w.r.t. S.
Otherwise by the induction hypothesis, we must have

S| i ∪ 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| ⊥ |= C ′ .
The second part of the lemma follows immediately by a straightforward induction (since

S| [i,∞[ def = ∪ j≥i S| j ).
Definition 25 If i > 0, we denote by S| ⋆ i the set of non ground clauses of level i in S. If i = 0 then we define S| ⋆

0 def = S| 0 . ♢ Lemma 26 Let S be a k-reducible, set of normalized clauses. If i > k, then S| ⋆ i ∪ S| ⊥ |= S| i .
Proof. Let C ∈ S| i . Since S is k-reducible, there exists a derivation of C from a set of k-normalized clauses. Furthermore, every clause in this derivation is levelredundant w.r.t. S. We prove, by induction on the length of the derivation, than for every clause C ′ of level i occurring in the derivation, we have

S| ⋆ i ∪S| ⊥ |= C ′ . The proof is obvious if C ′ is non ground. If C is ground, since i > k, C
′ must be deduced from two clauses D 1 and D 2 by resolution (or factorization). Furthermore, by Lemma 18, D 1 and D 2 are of level i or ⊥. By the induction hypothesis we have

S| ⋆ i ∪ S| ⊥ |= D 1 , D 2 |= C ′ .
Proposition 27 Let S be a set of clause. Let C be a clause such that C ⊑ l S.

Let i be the level of C.

If C is not ground then C ⊑ l S| ⊥ ∪ S| ⋆ i .
Proof. By definition there exist n clauses C 1 , . . . , C n of level ⊥ or i such that for every substitution σ there exist n substitutions σ 1 , . . . , σ n such that Cσ 1 , . . . , Cσ n |= C and

C 1 θ 1 , . . . , C n θ n ≼ Cσ. Furthermore, since C is not ground, C 1 , . . . , C n are not ground. 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 n ∈ S| ⊥ ∪ S| ⋆ i and C ⊑ l S| ⊥ ∪ S| ⋆ i .
Lemma 28 Let S be a k-reducible set of normalized clauses and let i, j be natural numbers. If:

1. j ̸ = 0 and i > k.

2. S is saturated up to level i.

S|

⊥ ∪ S| ⋆ i+j |= shift(S| ⋆ i , j). Then: S is satisfiable iff S ∪ {n < i + j} is. n < i + j is called a pruning clause for S. Proof. Let S ′ = S| [⊥,i[ ∪ ∪ l≥i S| ⋆ l . By definition we have S| l = S ′ | l if l < i, and S ′ | l = S| ⋆ l if l ≥ i. Furthermore, since S is k-reducible, S ′ is also k- reducible.
Finally, by Lemma 26 we have S ≡ S ′ . Hence it suffices to show that S ′ ∪ {n < i + j} is satisfiable. We prove that S ′ satisfies the application conditions of Lemma 22.

1. S ′ is saturated up to level i. Let C be a clause deduced from clauses in S ′ | [⊥,i[ = S| [⊥,i[ . Since S is saturated up to level i, C is level-redundant with respect to S. Hence C ⊑ l S. If the level of C is strictly lower than i we deduce that C ⊑ l S| [⊥,i[ hence C ⊑ l S ′ . Otherwise, by Lemma 18, C is non ground, thus C ⊑ l S| ⊥ ∪ S| ⋆ i by Proposition 27. 2. S ′ | i ∪ S ′ | ⊥ |= S ′ | [i,∞[
. This is a direct application of Lemma 24.

3. S ′ | i contains no ground clause. If i = 0, then this is trivial since by definition there exists no ground clause of depth 0. If i > 0 then the result stems from the definition of

S| ⋆ i . 4. S ′ | ⊥ ∪ S ′ | i+j |= shift(S ′ | i , j). We have S| ⊥ ∪ S| ⋆ i+j |= shift(S| ⋆ i , j) and S| ⊥ ∪S| ⋆ i+j = S ′ | ⊥ ∪S ′ | i+j . Thus S ′ | ⊥ ∪S ′ | i+j |= shift(S| ⋆ i , j). Furthermore S| ⋆ i \ S ′ | i hence shift(S| ⋆ i , j) \ shift(S ′ | i , j).
In practice, Condition 3 may be difficult to check. A simple solution (that is sufficient for the termination result in the following section) is to check that S| ⋆ i+j = shift(S| ⋆ i , j) (up to a renaming of variables).

Example 29 Consider the clause set S = {1, . . . , 8} of Example 7 (generated from the formula p n ∧ (∀x p succ(x) ⇒ p x ) ∧ ¬p 0 ):

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

Hence the pruning rule applies and generates: n ̸ ≈ succ(succ(succ(x))), i.e. n < 3. Together with clauses 5, 6 and 8, we obtain a finite, purely equational, and unsatisfiable clause set. The unsatisfiability of this set can be tested by standard algorithms. Thus the initial clause set is unsatisfiable. ♣

Example 30 Consider the following schema:

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

1 p 0 (level ⊥) 2 ¬p x ∨ q x (level ⊥) 3 ¬q x ∨ ¬q succ(x) (level ⊥) 4 q x ∨ q succ(x) (level ⊥) 5 n ̸ ≈ x ∨ ¬q x (level 1) 6 n ̸ ≈ x ∨ ¬q succ(x) (level 0) q 0 (resolution 1,2) (level ⊥) 8 n ̸ ≈ 0 (resolution 7, 5) (level 1) 9 n ̸ ≈ succ(x) ∨ q x (resolution 5,4) (level 2) 10 ¬p succ(x) ∨ ¬q x (resolution 2, 3) (level ⊥) 11 n ̸ ≈ succ(succ(x)) ∨

Termination

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

Definition 31 A derivation with pruning 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 the following conditions holds:

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

• S i = S i-1 ∪ {C} where C is a pruning clause for S i-1 (pruning step).

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

In practice identifying all level-redundant clauses is unfeasible, thus we only delete the clauses that are valid or subsumed.

We write S ⊢ p C if there exists a derivation with pruning C 1 , . . . , C n from S such that C n = C.

Definition 32 A derivation with pruning of a clause set S is a derivation with pruning containing every clause in S (here S denotes the conclusions of the derivation). ♢

A derivation is non redundant iff the deletion steps are applied with the highest priority. It is fair iff for every C such that S ⊢ p C, there exists an i ∈ N such that C is redundant w.r.t. S i .

Lemma 33 Let (S i ) i∈I be a derivation with pruning from a k-normalized clause set. 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 has been deleted by a previous redundancy elimination step. In both cases C j must be level-redundant with respect to S i .

Corollary 34 Let (S i ) i∈I be a fair, non redundant derivation with pruning from a finite and normalized clause set. I is finite.

Proof. Since S 0 is finite and normalized, it must be k-normalized for some k ∈ ⊥ ∪ N. Assume that I is infinite. By Proposition 12, the number of distinct clauses of a given level is finite. Thus for every l, there exists an index γ(l) such that every clause that is generated after this step is of level strictly greater than l. Since I is infinite, γ is strictly increasing. Let l be a natural number strictly greater that the maximal number of distinct normalized clause sets of the same level.

For every m ∈ N, let S ′ m denote the set of clauses

C such that n ̸ ≈ succ m-1+ϵ (x) ∨ C ∈ S γ(l) | m , with x ∈ V. Obviously, S ′
m is a set of normalized clauses. Then by the pigeonhole argument, there exist i < l and j ̸ = 0 such that S ′ i = S ′ i+j . By definition, this implies that S γ(l) | ⋆ i+j = shift(S γ(l) | ⋆ i , j) (thus in particular S γ(l) | ⋆ i+j |= shift(S γ(l) | ⋆ i , j)). Furthermore, S γ(l) is saturated up to level i (since the derivation is fair and since no clause of level i or i + 1 can be deduced after step γ(l)). Thus the pruning rule applies on S γ(l) . Hence it also applies on S γ(l)+1 , . . .. By fairness it must be applied at some point, thus the clause n < i + j occurs in one of the S k . But then the number of non redundant clauses is finite since any clause of level ≥ i + j is subsumed by n < i + j.

Constructing the resolution proof

From the result of the previous sections, we know that a normalized clause set S is satisfiable iff a finite set of unsatisfiable purely equational clauses is derivable from S. In this section we show how to explicitly construct a resolution proof for S (which is needed for applying the cut elimination procedure in [START_REF] Baaz | Cut-elimination and Redundancy-elimination by Resolution[END_REF]). Since S is parameterized by a parameter n, so is its proof, which is actually a schema of (propositional) resolution proofs.

We introduce some notations. Let δ be a clause set or a derivation. If k ∈ N, we denote by δ[k] the clause set or derivation obtained by:

• Deleting from δ every clause of the form n ̸ ≈ t ∨ C such that k is not an instance of t.

• Replacing every clause n ̸ ≈ t ∨ C such that k = tσ by Cσ. Proof. The proof is by a straightforward induction on the length of δ.

The following lemma handles the (easy) case of the derivations without pruning.

Lemma 38 Let S be a normalized clause set and let δ be a refutation of S. Let (∆ k ) k∈N be the family of derivations defined by ∆ k

def = δ[k]. If δ does not contain any application of the pruning rule then ∆ k is a refu- tation of S[k].
Proof. This is an immediate consequence of Proposition 37.

Let δ be a derivation with pruning from a clause set S. We may assume that δ contains only one application of the pruning rule (this is sufficient to ensure termination, as shown in Section 6). We denote by i δ and j δ the natural number i, j corresponding to the application of the pruning rule in δ (as defined in Lemma 28). We denote by S δ the set of clauses on which the pruning rule is applied and by T δ the set:

T δ def = S δ | ⋆ i ∪ S| ⊥ .
Lemma 39 Let S be a set of normalized clauses and let δ be a refutation with pruning of S. Let δ ′ be the greatest subderivation of δ from T δ . Let (∆ k ) k∈N be the family of derivations defined as follows: ). Again, we distinguish two cases, according to the value of k.

• ∆ k def = δ[k] if k < i. • ∆ k def = δ[k].Γ k if k ≥ i where: -Γ k def = δ ′ [k] if k < i + j -Γ k def = δ ′ [k].Γ k-j if k ≥ i + j ∆ k is a refutation of S[k]. Proof. If k < i,
• Assume firstly that i ≤ k < i + j. By definition, δ ′ [k] is a derivation from T δ [k]. δ must contain a clause of the form n ̸ ≈ k.
This clause is of level greater than i, thus must be deducible form T δ , as shown in the proof of Lemma 24. Hence δ ′ is a derivation of n ̸ ≈ k and δ

′ [k] is a refutation of T δ [k].
• Now assume that k ≥ i + j. Every clause in S δ | ⋆ i+j is deducible from T δ (as shown by Lemma 24). Thus δ ′ is a derivation from T δ of S δ | ⋆ i+j . By definition of the pruning rule, we have

S δ | ⋆ i+j = shift(S δ | ⋆ i , j). Hence δ ′ is a derivation from T δ of shift(S δ | ⋆ i , j), thus δ ′ [k] is a derivation of shift(S δ | ⋆ i , j)[k]. We have T δ = S δ | ⋆ i ∪ S δ | ⊥ . By Proposition 36 S δ | ⋆ i [k -j] is equal to shift(S δ | ⋆ i , j)[k]. Hence δ ′ [k] is a derivation of S δ | ⋆ i [k -j]. Thus δ ′ [k] is a derivation of S δ | ⋆ i [k -j] ∪ S δ | ⊥ hence of T δ [k -j]. But by the induction hypothesis Γ k-j is a refutation of T δ [k -j]. Thus δ ′ [k].Γ k-j is a refutation of T δ [k].

Expressive power

Although the class of normalized clause sets is strongly restricted from a syntactic point of view it is actually rather expressive. We show how to encode literals that are outside the class into normalized clause sets.

Encoding translation on indices

We first consider atoms of the form p succ k (x) (where k ∈ N). Such formulae are encoded by a new predicate symbol p k

x , with the intended meaning that p k x ⇔ p succ k (x) . The following axioms ensure that p k

x have the intended interpretation:

A k def = {p l x ⇔ p l-1 succ(x) , p 0 x ⇔ p x | k ≥ l > 0}.
Notice that A k is finite and normalized. We have the following:

Proposition 40 If I |= A k then for every l ∈ [0, k], I |= (p l x ⇔ p succ l (x) ). Proof. By a straightforward induction on l.

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 ′ is the set of clauses of the form: q l,ϵ,k x ⇔ q 0,ϵ,k succ l (x) q 0,ϵ,k+1 succ(x) ⇔ q 0,ϵ,k x ¬q 0,ϵ,k 0 q 0,0,0

n ̸ ≈ x ∨ q 0,1,0

n ̸ ≈ x ∨ ¬q 0,1,0 x q 0,1,0 succ(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 succ k (x) in the first axiom, but obviously one can apply the previous transformation to obtain an equivalent normalized formulation.

Proposition 41 Let I |= A ′ l ′ ,k ′ . For every (l, k, ϵ) ∈ [0, l ′ ] × [0, k ′ ] × {0, 1}, we have I |= q l,ϵ,k x ⇔ x + l > ϵ.n + k.

Proof. Assume that l = k = 0. If ϵ = 0 then the interpretation of q l,ϵ,k is fixed by the third and fourth axioms and we have indeed q 0,0,0 succ(x) (i.e. succ(x) > 0) and ¬q 0,0,0 0 (i.e. 0 ̸ > 0). If ϵ = 1, then the interpretation of q l,ϵ,k is fixed by the fifth and sixth axioms that state that we have q 0,1,0 succ(x) if x = n (i.e. succ(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 x is true (resp. false) if x > s(n) (resp. x < n). By using the second and third axiom 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 formulae 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.

Encoding schemata with several parameters

The restriction to one parameter only is also non restrictive. 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 are defined by atoms r l x , defined by the following formulae A ′′ : ¬r l

x ∨ r l succ(x)

¬r l 0 n ̸ ≈ x ∨ r l succ(x)
where l ∈ [1, k].

Notice that the obtained formula is normalized.

Proposition 42 If I |= A ′′ then for every l ∈ [1, k] there is exactly one natural number n l such that I |= r l x iff x > n l . Furthermore, n l ≤ n.

Proof. Let n l be the lowest natural number such that I |= r l succ(n l ) . n l exists since r l succ(n l ) holds (by the third axiom). We have I |= ¬r 0 l , thus by minimality of n l r l n l cannot hold. Then by using the first axiom we show that I |= r l x for every x > n l and that I |= ¬r l

x for every x ≤ n l .

Then the formula x ≈ n l is written x + 1 > n l ∧ x ̸ > n l . ψ 0 ⇔ false

Inductive definitions

ψ x+1 ⇔ ϕ x-1+a ∨ ψ x .
After translation into clausal normal form and after removing the translation as explained in Section 8.1, one gets a normalized clause set.

Regular schemata

Using the previous transformations it is easy to prove that every regular schema 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 equisatisfiable (every model of S is also a model of ϕ and every model of ϕ can be extended into a model of S). Furthermore, the size of S is linear w.r.t. the one of ϕ (if natural numbers are encoded as unary terms in the original schema2 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 ∧ ∞ i=0 p i is easily expressed by the normalized clause set {p i } but it is not a regular schema (due to the unbounded conjunction).

1 and

 1 Lemma 17 If S is set of normalized non valid clauses then any non valid clause in R(S) is normalized. Proof. Let C be a (non valid) clause deduced from two normalized clauses D 1 and D 2 by resolution. By definition, D in 1 and D in 2 are of the form p u1 ∨ D ′ ¬p u2 ∨ D ′ 1 where u 1 and u 2 are unifiable. Let D

  To help the reader to grasp the next 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 10) . Notice that by Lemma 18, the clauses in S ′ | k (where k > 0) must be generated either from clauses in S ′ | k ∪ S ′ | ⊥ or from S ′ | k-1 ∪ S ′ | ⊥ (except of course those that already occur in the original clause set S). By definition of the notion of level, each of these sets S ′ | k can be viewed as a formula of the form n ̸ ≈ succ k (x) ∨ S k , where S k is a conjunction of xclauses 1

  then every index in D ′ θ must be lower or equal to I(n)ij + 1. By definition of J, this implies that I and J coincide on (l u ∨ D ′ )θ. If D ′′ is empty, then we have D = l u ∨ D ′ , and the proof is completed since by hypothesis J |= Dθ, thus J |= (l u ∨ D ′ )θ and I |= (l u ∨ D ′ )θ. Otherwise, D ′′ is of the form n ̸ ≈ succ l (t). Since J ̸ |= D ′′ θ we have J

  Intuitively the clauses in S[k] are exactly those obtained by fixing the value of the parameter n to k. Notice that the clauses in δ[k] are standard clauses (with no parameter). We have the following: Proposition 35 Let S be a set of clauses. Let I be an interpretation. I |= S iff I |= S[I(n)]. Proof. This follows immediately from the definition. Thus a set of clauses S is satisfiable iff there exists a natural number k such that S[k] is satisfiable. The set {S[k] | k ∈ N} is the family of (standard) clause sets denoted by the schema S. Our goal is to construct, from a refutation of S, a family of refutation (without pruning) of every clause set S[k]. Proposition 36 For every set of non parameter-free and non ground clauses S and for every pair of natural number k, j such that k ≥ j, we have shift(S, j)[k] = S[kj]. Proof. By definition shift(S, j) is the set of clauses of the form n ̸ ≈ succ i+j (x)∨ C, where x ∈ V and n ̸ ≈ succ i (x) ∨ C ∈ S. Notice that every clause in S must have the form n ̸ ≈ succ i (x) ∨ C where i ∈ N and x ∈ V. Thus shift(S, j)[k] is the set of clauses of the form Cσ, where succ i+j (x)σ = k, i.e. the set of clauses of the form C{x → kj -i} where n ̸ ≈ succ i (x) ∨ C ∈ S and i ≤ kj. This last set of clauses is exactly S[kj]. Proposition 37 Let S be a set of normalized clauses. If δ is a derivation from S, then δ[k] is a derivation (in the usual sense) from S[k].

Now, consider an

  inductive definition: ϕ 0 ⇔ B and ϕ k+1 ⇔ I if k ≥ 0 where B and I denotes formulae and where I contains atoms of the form p k or p succ(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 ϕ succ(x) ⇔ I. 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 are easily encoded by an atom ψ b-a+1 = ∨ b-a+1 x=1 ϕ x-1+a defined as follows:

  This clause is strictly smaller than Dθ and false in J. Since S is saturated up to level i,(E ′ ∨ E ′′ ∨ D ′ ∨ D ′′ )σ is level-redundant in S. Thus there exist m clauses C 1 , . . . , C m ∈ S and m substitutions σ 1 , . . . , σ n such that C 1 σ 1 , . . . , C m σ m ≼ (E ′ ∨E ′′ ∨D ′ ∨D ′′ )σ and C 1 σ 1 , . . . , C m σ m |= (E ′ ∨E ′′ ∨D ′ ∨D ′′ )σ. By Lemma 18, (E ′ ∨E ′′ ∨D ′ ∨ D ′′ )σ is of level at most i, thus so are C 1 , . . . , C m . If C 1 , . . . ,C m are of level i then we must have J |= C 1 , . . . , C m by the first item above. Otherwise, by the minimality condition on Dθ, we have J |= C 1 σ 1 , . . . , C m σ m . In every case we deduce that J |=

  Let i = 2, j = 2. Let S ′ = {1-18}. S ′ is saturated up to level 2. We haveS ′ | ⋆ 2 = {9, 15}, S ′ | ⋆ 4 = {13, 18}. One can easily check that shift(S| ⋆ 2 , 2) = S| ⋆ 4 .Thus the looping rule applies and generates: n ̸ ≈ succ(succ(succ(succ(x)))) i.e. n < 4. Together with the clauses 8, 10, 12 and 19, this yields a finite, purely equational, unsatisfiable, clause set. ♣

	¬q x	(resolution 9, 3)	(level 3)
	12 n ̸ ≈ succ(succ(0))	(resolution 11, 7) (level 3)
	13 n ̸ ≈ succ(succ(succ(x))) ∨ q x	(resolution 11, 4) (level 4)
	14 n ̸ ≈ x ∨ q x	(resolution 4, 6)	(level 1)
	15 n ̸ ≈ succ(x) ∨ ¬q x	(resolution 3, 14) (level 2)
	16 n ̸ ≈ succ(0)	(resolution 7, 15) (level 2)
	17 n ̸ ≈ succ(succ(x)) ∨ q x	(resolution 4, 15) (level 3)
	18 n ̸ ≈ succ(succ(succ(x))) ∨ ¬q x (resolution 17, 3) (level 4)
	19 n ̸ ≈ succ(succ(succ(0)))	(resolution 18, 7) (level 4)

  then the proof is an immediate consequence of Proposition 37. If k ≥ i, we show (by induction on k) that Γ k is a refutation of T δ [k]. This is sufficient to obtain the desired result since, by Lemma 24, each clause in T δ occurs in δ (thus δ[k] is a derivation of T δ [k]

Otherwise a schema as simple as p 1 0 . . . 0 n could not encoded in linear size).