# primal_grammars_driven_automated_induction__df227f4d.pdf

Primal Grammars Driven Automated Induction

Adel Bouhoula1 and Miki Hermann2

1Arabian Gulf University, Bahrain 2LIX, CNRS, Ecole Polytechnique, Institut Polytechnique de Paris, France a.bouhoula@agu.edu.bh, hermann@lix.polytechnique.fr

Automated induction is a powerful method for the validation of critical systems. However, the inductive proof process faces major challenges: it is undecidable and diverges even with small examples.

Previous methods have proposed ad-hoc heuristics to speculate on additional lemmas that hopefully stop the divergence. Although these methods have succeeded in proving interesting theorems, they have significant limitations: in particular, they often fail to find appropriate lemmas, and the lemmas they provide may not be valid.

We present a new method that allows us to perform inductive proofs in conditional theories. This method automatically detects divergence in proof traces and derives primal grammars as well as new lemmas that schematize the divergent sequence. This new construction allows us to break the divergence and complete the proof.

Our method is presented as a set of inference rules whose soundness and refutational completeness have been formally proved. Unlike previous methods, our method is fully automated and has no risk of over-generalization. Moreover, our technique for capturing and schematizing divergence represents the most general decidable schematization, with respect to description power, among all known schematizations.

Our method has been implemented in C++ and successfully proved over fifty complex examples that fail with well-known theorem provers (e.g., ACL2, Isabelle, PVS, SPIKE) and related methods for handling divergence in proofs by induction.

Our method represents a significant contribution to the field of automated reasoning as it can be integrated with existing automated and interactive inductive proof systems to enhance their performance. Moreover, it has the potential to substantially reduce the time needed for the verification of critical systems.

1 Introduction

Proof by induction is more and more frequently adopted for certifying critical hardware and software. Its power is expressed by the successes of the Boyer-Moore theorem prover Nqthm [Boyer and Moore, 1979], that has been considered for many years as the only significant automated theorem proving system for induction. Other inductive theorem provers have also been developed like SPIKE [Bouhoula and Rusinowitch, 1993], RRL [Kapur and Zhang, 1995], PVS [Rushby et al., 1998], ACL2 [Kaufmann et al., 2000] (successor version of Nqthm), LEAN [de Moura and Ullrich, 2021], and Vampire [Hozzov a et al., 2021]. Unfortunately, very often they present an undesirable phenomenon called divergence, where new subgoals are generated over and over again, without finally terminating with the required goal, which is a proof or a disproof of the initial conjectures. This phenomenon is present even in the case of very small examples. Previous methods have proposed ad-hoc heuristics to speculate on additional lemmas that hopefully stop the divergence. Although these methods have succeeded in proving several interesting conjectures, they have significant limitations: the provided lemmas may not be valid in the initial model of the axioms, and they often fail to find appropriate lemmas. In this case, the user will manually try to find the necessary lemmas. It is a very tedious process, and results are not guaranteed. Our approach is new in several aspects. The proof procedure does not require to be stopped but proceeds automatically by detecting the divergence of proof traces and deriving a primal grammar that schematizes the divergent sequences. It suggests some new lemmas that subsume all conjectures of the divergent sequence and allow the proof procedure to automatically discard them, continuing the proof with the new lemmas. Our method is presented as a set of inference rules whose soundness and refutational completeness has been formally proved. Refutational completeness is particularly useful for debugging programs and detecting flaws in security protocols. Since divergence is undecidable in general, we do not pretend that our procedure produces a result in every case. However, if the divergent sequence of clauses, produced during an inductive proof, follows a primitive recursive pattern, our approach always produces a correct and complete schematization by a primal grammar, which allows to stop the divergent process and successfully terminate the proof. Integrating

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

primal grammars and the new lemmas into the proof procedure preserves refutational completeness and avoids the risk of over-generalization. Our method has been implemented in C++ and successfully proved over fifty complex examples in a completely automatic way, unlike related provers, which require user interaction or ad hoc heuristics or fail, since it is not always possible to speculate on additional lemmas to complete a proof. The main advantages of our method compared to related work are: (i) it is completely automatic, i.e., no interaction with the user, (ii) it deals with conditional axioms, (iii) it preserves refutational completeness, (iv) there is no risk of overgeneralization, Our method represents a major development in the field of automated reasoning as it can be integrated with existing automated and interactive inductive proof systems to enhance their performance. Moreover, computer experiments show that our method has the potential to significantly reduce the time needed for the verification of critical systems. The paper is organized as follows. Section 2 presents related work for both solving the divergent issues of proofs by induction and schematization of divergence, together with our motivation. Section 3 introduces the necessary preliminaries and notation. In Section 4 we define our method of primal grammars for capturing divergence, together with the algorithm generating them from a divergent sequence of clauses. Section 5 explains the construction of a primal grammar from a divergent sequence. Section 6 introduces inductive positions and test sets. Section 7 presents our inference system to perform inductive proofs with the help of primal grammars. Section 8 summarizes the results of our computer experiments and shows the effectiveness of our new method through two illustrative examples. More examples can be found at the github page https://github.com/Bouhoula Hermann/IJCAI-2024.

2 Related Work

Several methods have been proposed to avoid or stop the divergence of rewriting-based inductive provers in unconditional theories. Most of them consist of stopping the prover in his divergent behavior and either manually or using adhoc heuristics to speculate on additional lemmas or to discover generalizations, which hopefully stop this unwanted phenomenon: the primary term heuristic [Aubin, 1976], the rippling heuristic [Bundy et al., 1993], the difference matching procedure [Basin and Walsh, 1992; Basin and Walsh, 1993], the divergence critic [Walsh, 1996], the use of proof planning [Ireland and Bundy, 1996], the speculate heuristic [Kapur and Subramaniam, 1996], the generalization of conjectures [Urso and Kounalis, 2004], and the induction with generalization [Hajd u et al., 2020]. Although these methods have succeeded to prove several interesting theorems, they have important limitations: First, they may require high user guidance. Second, there are no guarantees against over-generalization (except in [Urso and Kounalis, 2004] under some conditions) and provided lemmas may not be valid in the initial model of the axioms. Third, attempting to prove the lemmas themselves can cause

fresh divergence. Several researchers in the 1990s noted that the infinite behavior during theorem proving, called divergence, follows a primitive recursive pattern. To cope with this phenomenon, they proposed different schematizations. Most notable among them and in their order of increasing schematization power are those of [Chen et al., 1990], [Salzer, 1992], [Comon, 1995], and [Hermann and Galbav y, 1997]. However, up till now nobody proposed to synthesize primal grammars from divergent proofs. Subsequently, there is no previous work on maintaining refutational completeness in the presence of schematizations. To guarantee that our method can handle a very large class of specifications and conjectures, we have developed a new version of primal grammars based on Presburger arithmetic. These grammars represent the most general decidable schematization, with respect to description power, among all known schematizations. Certainly, as the divergence of equational proofs is undecidable in general, not all divergent sequences can be schematized by primal grammars. We can only consider those presenting a primitive recursive behavior, which allows us to cover a large class of problems. It is important to note that the Ackermann function for example fails to be captured by primal grammars since it is not compatible with primitive recursion. In this paper, we propose a new method for proof by induction in conditional theories. Our method automatically detects the divergence of proof traces and derives a primal grammar, as well as new lemmas that subsume all conjectures of the divergent sequence. This allows the proof procedure to automatically discard them and continue the proof with the new lemmas. Our method has been implemented and the numerous computer experiments show that our method is very promising and can significantly contribute to shortening the time needed to validate critical systems.

3 Preliminaries

We introduce the main notation used later and refer to [Dershowitz and Jouannaud, 1991; Bouhoula, 1997; Baader and Nipkow, 1998; Bouhoula, 2009] for the details and missing definitions. We always assume that we are working within a quantifier-free first-order language with equality. A many-sorted signature Σ is a pair (S, F) where S is a set of sorts and F is a finite set of function symbols, partitioned into two disjoint subsets: the first one C, contains the constructor symbols and the second D, is the set of defined symbols. Let X be a countably infinite set of variables and let T(F, X) be the set of well-sorted F-terms. A ground term has no variables. T(F) denotes the set of ground terms. A position a of a term t T(F, X) is a string of natural numbers which is an index of a subterm in a tree representing t. Pos(t) denotes the set of all positions of a term t. FPos(t) denotes the subset of Pos(t) containing only the functional positions in t. Two positions a and b of a term t are parallel if a is not a prefix of b, nor b is a prefix of a. A set of positions A is called parallel if any two positions a, b A are parallel. A subterm

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

of t at position a Pos(t) is denoted by t|a. An equation is a pair of the form t1 = t2, where t1 and t2 are terms of the same sort. A conditional equation is either an equation or an expression of the form e1 en e, where e, e1, . .. , en are equations, with e1, . . . , en being the conditions and e is the conclusion. A clause is an expression of the form e1 en e 1 e m. Axioms are built from conditional equations. Goals to be proved are clauses. A term t is an instance of t if there is a substitution σ such that t = t σ. A variable renaming is an injective substitution σ: X X, such that its domain and range are disjoint for a finite subset of variables X X, for which xσ = x holds. Two terms s and t are equivalent modulo variable renaming if s is an instance of t and t is an instance of s. We denote by Vars(t) the variables of a term t. A rewrite rule l r is an oriented equality such that l T(F, X) X and Vars(r) Vars(l), where Vars(t) is the set of variables of t. In addition, we require the relation l r to hold where is a well-founded ordering on terms. A term rewriting system is a set of (conditional) rewrite rules. Given a term rewriting system R, a reduction relation R on terms is defined as s R t if there is a (conditional) rule c l r and a substitution σ, such that l c, lσ is a subterm of s and for each equation in the condition c of the form a = b, the instances aσ and bσ reduce to the same normal form, Then t is obtained by replacing the subterm lσ by rσ in s. We denote by t R the normal form of the term t obtained by reduction using a confluent and terminating rewrite system R. A term t is R-irreducible if there is no term s such that t R s. A substitution σ is R-irreducible if xσ is Rirreducible for any variable x of its domain. We say that two terms s and t are joinable if s R v and t R v hold for some term v. A formula φ is a deductive theorem of E if it is valid in any model of E, denoted by E |= φ. The rewrite relation R is said to be ground convergent if the terms u and v are joinable whenever u, v T(F) and R |= u = v. Given a set of axioms E and a clause c called a conjecture, we want to prove that c is an inductive consequence of E, i.e., any ground instance of c is a consequence of E. In order to establish consequence relations, we consider initial models. We write E |=ind c, if c is valid in the initial model of E. Any ground instance cσ such that E |= cσ is a counterexample. A clause c is not valid in the initial model of E if there is a ground instance of c which is a counterexample. The deduction relation |=ind extends to sets of equalities as follows: E |=ind Φ holds if E |=ind e for every e Φ. Let T(C) be the set of ground terms constructed from the signature C. An operator f D is sufficiently complete if for all t1, . . . , tn T(C), there exists t T(C) such that f(t1, . . . , tn) R t. If each f D is sufficiently complete then we say that R is sufficiently complete. Let f D be a sufficiently complete defined function. If for all rewriting rules ci f(t1, . . . , tn) ri whose left-hand sides are identical up to a variable renaming σi, we have c1σ1 cnσn valid in the initial model of R, then f is strongly complete with respect to R. We say that R is strongly complete if any function symbol in D is strongly complete with respect to R.

4 Capturing Divergence

Divergence in equational proofs is undecidable in general, since we can simulate the work of a Turing machine by means of superposition and reduction during a proof derivation. This fact implies that we can search only for sufficient conditions to detect and capture divergence. An appropriate tool for capturing divergence is the formalism of primal grammars [Hermann and Galbav y, 1997]. Primal grammars are based on primitive recursive functions adapted for term rewriting systems. They represent the most powerful schematization of divergent systems in terms of inclusion. However, if a proof derivation presents a fast-growing behavior beyond the class of primitive recursive functions, like for instance the Ackermann function, there exists no reasonable general purpose mean to cope with such type of divergence, except the design of an ad-hoc schematization. For the needs of primal grammars, the signature F consists of constructors K, defined symbols D, where K and D are disjoint, and the special symbols + (addition), plus the constants 0 and 1. The defined symbols are surmounted by a hat to distinguish them from the constructors. We also need the set of counter variables C, disjoint from ordinary variables X. Note that constructors for primal terms are different from constructors in inductive proofs. The arguments of the defined symbols are divided into two parts by a semicolon. Those before the semicolon are called counters. Each defined symbol ˆf has a counter arity car( ˆf). The manipulation of counters is based on the counter expressions N(C). They are the smallest algebra containing 0, the counter variables C, and closed under the application of addition by 1. Since this algebra is isomorphic to linear expressions over natural numbers, we use the arithmetic expressions c + 1 and c + k for the addition by 1 and the addition by k. The schematization level is represented by the algebra of primal terms P = (K, D; C, X), which is the smallest set such that: (1) X P, (2) if c1, . . . , ck N(C), t1, . . . , tn P, and ˆf D with car( ˆf) = k and ar( ˆf) = n, then ˆf(c1, . . . , ck; t1, . . . , tn) P, (3) if t1, . . . , tn P and f K with ar(f) = n then f(t1, . . . , tn) P. The approximation of ˆf(c; t) with respect to a precedence on D is the set Apx( ˆf(c; t)) = {ˆg(z; u) | ˆf ˆg}, where z is a subsequence of c and u is a subsequence of t. The set of positions occupied by defined symbols in a term t is denoted by DPos(t). A wrap of a primal term t is the context Wrp(t) = t[ ]DPos(t) where each subterm at every position DPos(t) of a defined symbol is replaced by a hole, a special constant absent from any set of symbols F. A depth d iteration (or d-iteration) of a wrap w = w[ ]A, denoted by w A d for d N, is defined as w A 1 = w and w A i+1 = w[w A i]A. A d-iteration of a wrap w = w[ ]A modulo variable renaming, denoted by w d A d, is recursively defined by w 1 A 1 = w and w i+1 A i+1 = wi+1[w i A i]A, where all wi[ ]A, i N, are equivalent modulo variable renamings with disjoint ranges.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

Primal terms are constructed to represent infinite sets of terms. Their semantics is defined by Presburger systems. Definition 1. Let be the precedence on the defined symbols D. With every defined symbol ˆf we associate two primal terms r1 and r2. The Presburger rewrite system R contains for each ˆf D the following pair of rewrite rules:

the basic rule ˆf(0; x) r1 or ˆf(0, c; x) r1

and the inductive rule, having one of the following forms: ˆf(n + 1; x) r2[ ˆf(n; x)]A or ˆf(n + 1, c; x) r2[ ˆf(n, c; x)]A or ˆf(n + 1, c; x) r2[ ˆf(n, c + 1; x)]A. where

c is a counter variable, and

x is a vector of ordinary variables,

A is a subset of parallel non-root positions in r2,

both terms r1 and r2 at every position from DPos(r1) and DPos(r2) belong to Apx( ˆf(n, c; x)),

the root symbol of r2 is a constructor,

each ordinary variable in x occurs in Wrp(r1) Wrp(r2). A Presburger system is designed as a primitive recursive function over the set of terms T(F, X). Each Presburger system is confluent and terminating [Hermann and Galbav y, 1997]. An enumerator for a primal term t is a ground substitution ξ : C N that instantiates all counter variables of t by natural numbers. The enumeration Ξ(t) is the set of all possible enumerators of t. A primal term represents the folded form of all terms in the schematized set S and an enumerator selects one element from S. A Presburger system R provides us with the machinery for computing the elements of a schematized set from a primal term t by instantiation tξ by a enumerator ξ Ξ(t), followed by reduction to normal form tξ R. Definition 2. A primal grammar is a quadruple G = (K, D, R, t), where K are the constructors, D are the defined symbols, R is a Presburger rewrite system, and t is a lemma. The language generated by a primal grammar is the set L(G) = {tξ R| ξ Ξ(t)}. We say that the primal grammar G schematizes the set L(G). The lemma t in the aforementioned definition can also be an equation or a clause, as it is the case in the scope of theorem proving. We put a bar on top of the primal term to distinguish it as the starting point of the primal grammar. We need to define the sets of terms to which primal grammars correspond. Definition 3 (Primitive Recursive Set of Terms). A countably infinite set of terms T is called 0-level primitive recursive if it can be arranged in an infinite sequence t0, t1, t2, . .. , tn, . .. and there exists a set of parallel positions A, such that

r1 is the first term t0 of the set T,

the equality ti = ti+1|a holds for every i N and each position a A,

there exists a wrap r2[ ]A such that ti A i = r i 2 A i.

A countably infinite set of terms T is called ℓ-level primitive recursive if it can be arranged in an infinite sequence t0, t1, t2, . . ., tn, . . . and there exists a set of parallel positions A, such that

r1 is the first term t0 of the set T,

the equality ti = ti+1|a holds for every i N and each position a A,

there exists a superset of parallel positions B A,

there exists a wrap r2[ ]B such that ti B i = r i 2 B i,

for each position b B A there exists a k-level primitive recursive set of terms T b, where k < ℓ,

ti|b = tb i holds for every i N and each position b B A, where tb i T b is the ith term in the sequence of T b.

A concatenation of an ℓ-level and a k-level primitive recursive sets T ℓ= {tℓ 0, tℓ 1, . . .} and T k = {tk 0, tk 1, . . .} with k < ℓis a primitive recursive set T = {t 0, t 1, . . .} if there exists two sets of parallel positions A and B, such that t i = tℓ i A i[tk i ]B for each i N.

A combination of a finite number of primitive recursive sets T0, T1, .. ., Tn is a primitive recursive set T = {t0, t1, . . .} if there exists mutually parallel sets of parallel positions Ai and a wrap w[ ]A such that ti = w[t0 i ]A0 [tn i ]An where tj i is the ith term in the sequence Tj for j = 0, . . . , n.

A countably infinite set of terms T is primitive recursive if it is ℓ-level primitive recursive for some ℓ N, a concatenation, or a combination of primitive recursive sets. Remark. Experimental observations show that each divergent sequence of clauses in an inductive proof is a primitive recursive set. The requirement that consecutive wraps must be equivalent modulo variable renaming takes care of rolling variables which may occur by instantiation of induction variables by the terms from the test sets (see Section 6). In the concatenation of two primitive recursive sets T ℓand T k a term ti T ℓis paired with a term t i T k at the same index i. Note also that all (ordinary) variables in each primitive recursive set T are always considered Skolemized, i.e., they cannot be instantiated. Example 4. The following finite prefix of a primitive recursive set of terms T has been produced during an inductive proof of the conjecture len(app(x, x)) = len(x) + len(x) over a specification of a list with the operations zero 0, successor s, addition +, empty list nil, concatenation cons, and application app. We obtained the following equations:

len(app(y, cons(x1, y))) = s(len(y)) + len(y), len(app(y, cons(x2, cons(x1, y)))) = s(s(len(y))) + len(y), len(app(y, cons(x3, cons(x2, cons(x1, y))))) = s(s(s(len(y)))) + len(y).

There is first the 0-level primitive recursive set T0 = {s(len(y)), s(s(len(y))), s(s(s(len(y)))), . . .} with the set of positions1 A = {0} and the wrap s( ). There is another 0-level primitive recursive set

T1 = {cons(x1, y), cons(x2, cons(x1, y)), cons(x3, cons(x2, cons(x1, y))), . . .}

with the set of positions A = {1} and the wrap cons(x, ) with variable renamings σi = [x xi]. They are then combined into the resulting primitive recursive set using the wrap

1All indices begin with 0.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

len(app(y, )) = s( ) + len(y). The variable x taking the indices 1, 2, 3, etc, is a so-called rolling variable. The following finite prefix of a primitive recursive set of terms T has been produced during an inductive proof of the associativity conjecture x + (x + x) = (x + x) + x over a specification of natural numbers with the operations of zero 0, successor s, and addition +. We obtained the equations x + s(x + s(x)) = (x + s(x)) + s(x),

x + s2(x + s2(x)) = (x + s2(x)) + s2(x),

x + s3(x + s3(x)) = (x + s3(x)) + s3(x). There is first the 0-level primitive recursive set T0 = {s(x), s2(x), s3(x), . . .}, followed by a 0-level primitive recursive set T1 = {s(x + y), s2(x + y), s3(x + y)}, both with positions A = {0} and wrap s( ). They are concatenated into a 1-level primitive recursive set T2 = {s(x + s(x)), s2(x + s2(x)), s3(x + s3(x)), . . .} using the position B = {0.1}. Finally the sets T0 and T2 are combined using the wrap x + = (x + ) + into the resulting primitive recursive set, where the first hole is replaced by T2 and the following two holes each by T0. Proposition 5. For each primitive recursive set of terms T there exists a primal grammar GT , such that L(GT ) = T.

Hint. Induction on levels ℓ N. Each level is assigned a different defined symbol ˆf. Descent to lower level is taken care of in the wrap r2[ ]A, concatenation is taken care of in r1, combination is taken care of in the lemma t.

Proposition 6. For each primal grammar G there exists a primitive recursive set of terms T such that L(G) = T.

Hint. Direct construction. The levels are determined by the ordering on defined symbols D.

5 Constructing a Primal Grammar Hermann and Galbav y defined primal grammars in [Hermann and Galbav y, 1997] and developed a unification algorithm for them, but they did not supply any procedure allowing to derive a suitable correct and complete primal grammar from an existing divergent sequence. In this section, we will formally develop the PRIMGRAM procedure performing exactly this necessary derivation. The first step in taming divergence is the design of a primal grammar GT = (KT , DT , RT , t T ) schematizing an infinite divergent sequence T = {t1, t2, . . .}, such that L(GT ) = T. Let Tp = {t1, t2, . . . , tp} T be a finite prefix of p initial terms of the divergent sequence T. To determine the maximal common wrap of a finite set of terms, we use the machinery of difference matching [Basin and Walsh, 1992] resp. difference unification [Basin and Walsh, 1993]. The PRIMGRAM function for deriving a primal grammar for a divergent sequence is presented in Algorithm 1. The details of the PRIMGRAM function are described as follows: (1) Determine the maximal common wrap w[ ]Q of the finite prefix Tp of the divergent sequence T by means of difference matching. This wrap consists of the term context common to all terms from Tp. Note that this wrap can have several holes on parallel positions Q.

(2) For each parallel position q Q, determine the corresponding divergent sequence of subterms T q p = {tq 1, tq 2, . . . , tq p}. For each i {1, . . . , p}, tq i is the subterm of ti at position q. Formally, tq i = ti|q for all ti Tp. (3) Using difference matching again, determine the maximal wrap r2[ ]A of T q p {tq 1} with holes at parallel positions A. (4) For each pair tq i , tq i+1 of consecutive terms from T q p , test if the subterm tq i+1|a at each position a A is equal to tq i . (5) If not, the finite prefix T q p of subterms T q from T at position q hides an encapsulated divergence. Recursively call this procedure on it, solve the encapsulated divergence by producing a primal grammar G = (K , D , R , t ) for T q, and replace this encapsulated divergent sequence in all terms from T q p by the lemma t . If the recursive call returns a failure, return it. (6) Check if the subterms tq 2|a at all positions a A are equal. If not, the maximal wrap r2[ ]A is wrong and return failure. If yes, put r1 tq 1. (7) Create the lemma t T for primal grammar GT from the maximal common wrap w[ ]Q by replacing the holes by corresponding primal term ˆfq(c; x) for each position q Q. (8) If there were encapsulated divergences encountered, which have now been replaced by the lemma te of their corresponding primal grammars Ge, incorporate the counters of te into actually created lemma t T q. Integrate the dependent primal grammars Ge into the created primal grammar GT q. Perform it for all parallel positions q Q. (9) By means of primal term matching of t T against the prefix Tp, determine dependency of counters.

Definition 7. A primal grammar G = (K, D, R, t) is a complete schematization for a primitive recursive set of terms T if for each term t T there exists an enumerator ξ Ξ(t), such that t = tξ R. A primal grammar G = (K, D, R, t) is a correct schematization for a primitive recursive set of terms T if for each enumerator ξ Ξ(t) there exists a term t T, such that t = tξ R.

The PRIMGRAM function for deriving a primal grammar for a divergent sequence is presented in Algorithm 1.

Theorem 8 (Correctness and Completeness). Let T be a primitive recursive set of terms. For each sufficiently long finite prefix Tp T, PRIMGRAM generates a primal grammar GT which is a correct and complete schematization of T.

Theorem 8 presents the statement that the PRIMGRAM function produces a primal grammar G which neither overgeneralizes a divergent sequence T, nor omits a term from T, i.e., that T = L(G) holds, provided that T is a primitive recursive set. The parameter p sufficient length of the prefix Tp is discussed further in the section on test sets. The following example illustrates Theorem 8.

Example 9. Suppose that PRIMGRAM receives the divergent sequence of clauses T = {a2(x) = true, a4(x) = true, a6(x) = true, . . .} which generalizes to a2k+2(x) = true. We will show that PRIMGRAM neither over-generalizes the sequence T, nor omits a term from T.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

Algorithm 1 Production of a primal grammar from a finite prefix of an infinite divergent sequence.

Input: Finite prefix Tp = {t0, t1, . . . , tp 1} of an infinite divergent sequence T. Output: Primal grammar GT = (KT , DT , RT , t T ) or failure. 1: function PRIMGRAM(Tp) 2: w[ ]Q maximal common wrap(Tp) 3: for all q Q do 4: T q p 5: for i = 0, . . . , p 1 do T q p T q p {ti|q}

6: r2[ ]A maximal common wrap(T q p {tq 0}) 7: for i = 0, . . . , p 2 do 8: for all a A do 9: if tq i+1|a = tq i then

10: (K , D , R , t ) PRIMGRAM(T q p ) 11: if PRIMGRAM(T q p ) = failure then 12: return failure 13: for j = 0, . . . , p 1 do tq j|a t

14: break 15: for all a1, a2 A do 16: if tq 2|a1 = tq 2|a2 then return failure

17: r1 tq 0 18: t T |q w[ ˆfq(c; x)]q 19: lift counters(t T |q)

20: match counters(t T , Tp) 21: return (KT , DT , RT , t T )

PRIMGRAM produces the Presburger system ˆf0(0; x) x, ˆf0(n + 1; x) a2( ˆf0(n; x))

and the lemma c = (a2( ˆf0(n; x)) = true). For every enumerator ξ, instantiating the counter variable n in the lemma c, there exists a corresponding clause in T. This means that the lemma a2( ˆf0(n; x)) = true subsumes the sequence T. Suppose that PRIMGRAM generated the Presburger system ˆf0(0; x) x, ˆf0(n + 1; x) a( ˆf0(n; x))

and the lemma c = (a( ˆf0(n; x)) = true) instead of the correct one. All clauses in T can be schematized by this primal grammar, but there exists, for instance, the enumerator ξ = {n 0} for which the instance c{n 0} reduces to the clause a(x) = true, which does not belong to T. A similar situation will happen with Presburger system whose inductive rule has the form ˆf0(n + 1; x) a2k+1( ˆf0(n; x)) for any k. Suppose now that PRIMGRAM generated the Presburger system ˆf0(0; x) x, ˆf0(n + 1; x) a4( ˆf0(n; x)) instead of the correct one. We cannot produce for example the clause a4(x) = true which belongs to T. A similar situation will happen with any Presburger system whose inductive rule has the form ˆf0(n + 1; x) a2k( ˆf0(n; x)) for k > 1.

We conclude that PRIMGRAM exactly captures all clauses in T. In this example, we assumed that T is infinite. However, in reality, PRIMGRAM takes only a finite prefix of T to generate the corresponding primal grammar. Since the sequence T contains a primitive recursive set below a maximal common wrap of all clauses, in this particular case of level 0, already a sufficiently long finite prefix Tp determines the required properties of the whole sequence T. According to Definition 3, we need to determine the set of parallel positions A, the wrap r2[ ]A which iterates through all positions A, and the term t0. The maximal common wrap w[ ]Q of T is a2( ) = true and Q contains a single position q = 0.0.0. This wrap will be used to construct the lemma. The terms T q below the wrap w[ ]Q are {x, a2(x), a4(x), . . .}. We need to show that Tq constitutes a primitive recursive set. The maximal common wrap r2[ ]A of T q is a2( ) with A = {0.0}. We have a2(x)|0.0 = x, a4(x)|0.0 = a2(x), etc, and also the equality a2i(x) 0.0 i = (a2(x) i 0.0 i for each i. The term r1 is equal to tq 0 which is x. Therefore T q is a 0-level primitive recursive set. From Definition 3 it follows that the set of parallel positions A, the wrap r2[ ]A, and the term r1 can be determined from a finite prefix of the primitive recursive set T. This example shows that PRIMGRAM generates exactly the equations of the form a2k+2(x) = true from a finite prefix of T. The following theorem shows that PRIMGRAM preserves refutational completeness. Theorem 10. Let c be a lemma in the primal grammar G = (K, D, R, c) generated by PRIMGRAM(T) from a primitive recursive set T and let R be a ground convergent rewrite system. Then R |= c implies R |= T.

Hint. Since c subsumes the sequence T, R |=ind c implies R |=ind T. This means that a counterexample for a clause in T is also a counterexample for c, and therefore we conclude that PRIMGRAM maintains the refutational completeness property.

6 Inductive Positions, Induction Variables, and Test Sets To perform a proof by induction, it is necessary to provide induction schemes. In our framework, these schemes are defined by a function, which, given a conjecture, selects the positions of variables where the induction will be applied (induction variables) and by a special set of terms called a test set which give us a finite description of the initial model of the rewrite system. Test sets are used to instantiate induction variables.

6.1 Induction Variables Induction variables are variables which may trigger a rewriting step when instantiated. Given a conditional rewrite system R, to compute induction variables, we start by the computation of induction positions of function symbols. This computation is done only once and permits us to determine whether a variable of a term t is an induction variable or not. Then, it is not necessary to consult the axioms in order to select the induction variables of a conjecture. For example, if

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

we consider the rewrite system {x + 0 x, x + s(y) s(x + y)}, then y is an induction variable of the term x + y, since the corresponding rewrite rules left-hand sides x + 0 and x + s(y) vary at the second position of +. We say also that 1 is an induction position2 of +. The inductive positions allow us to restrict the instantiation of conjectures to a smaller set of inductive variables that trigger a rewriting step. A sort S is finitary if the set of R-irreducible ground terms of sort S is finite. Otherwise, S is infinitary.

Definition 11 (Induction variables). The set Ind Var R(c) of induction variables of a clause c with respect to a rewrite system R is the smallest subset of Var(c) satisfying the following conditions: (1) if x is a variable of a finitary sort with respect to R then x Ind Var R(c); (2) if x = t|p, where t is a subterm of c of the form f(t1, . . . , tn), such that each ti is a term built from constructors and variables, and p is an inductive position of f, then x Ind Var R(c). If the rewrite system R is clear from the context, we denote the induction variables only by Ind Var(c).

6.2 Test Sets Let R be a left-linear conditional rewrite system. Let dp(R) be defined as the maximum depth of the left-hand sides of rules in R and dpf(R) be defined as the maximum depth of the left-hand sides of rules in R with the root symbol f. Let R be a sufficiently complete and ground convergent conditional rewrite system. Test sets are computed for all defined functions f. The test set TS[f, s] for a defined function f and a sort s is the set of all constructor terms of depths smaller or equal to dpf(R) with variables only on the deepest level. The test set TS is the union of all TS[f, s] for all defined functions f and all sorts s. A test substitution for a clause c instanciates induction variables of c by terms taken from a given test set whose variables are refreshed by renaming.

Example 12. Consider the rewrite system R with the rules

0 + x x, s(x) + y s(x + y), even(0) true, even(s(0)) false, even(s2(x)) even(x), even(x) = true odd(x) false, even(x) = false odd(x) true

where 0 and s are constructors of the sort nat, and +, even, and odd are defined functions. The final test set is equal to

TS = {(+, nat, {0, s(x)}), (even, nat, {0, s(0), s2(x)}), (odd, nat, )}.

7 Inference System for Proofs by Induction

In this section we describe an inference system I (see Figure 1) for proving or disproving inductive consequences with respect to a given conditional rewrite system R. The inference system operates on a tuple (E, H, G, T, S, B) where E is the set of conjectures, H is the set of induction hypotheses, G is the set of primal

2All positions start with 0 and proceed from left to right.

grammars, T is the list of new subgoals, S is the set of new signatures, and B is a Boolean flag.

The SIMPLIFY inference rule allows us to perform the following tasks.

Use of inductive rewriting to reduce a clause c with axioms from R, induction hypotheses from H, other conjectures from E that have not yet been proved and are smaller compared to c (which allows mutual simplification of conjectures), and primal grammars from G. We use a generalization of the complexity of equations given in [Bouhoula et al., 1995] to compare clauses. This complexity allows, in particular, to handle non-orientable equations.

Use of case rewriting.

Application of positive decomposition taking advantage of the fact that constructors are free to simplify clauses.

Delete redundant clauses or tautologies and application of occur check and negative clash if the constructors are free.

Subsume clauses modulo the equational theory generated by Presburger rewrite systems.

The INDUCTIVE NARROWING inference rule allows us to derive new subgoals by the instantiation of induction variable of a conjecture by the elements of test sets and the simplification of the obtained instances. Notation c :: T denotes pushing of c to the front of list T. The definitions of inductive rewriting, case rewriting, positive decomposition, occur check, and negative clash can be found in [Bouhoula, 1997]. The PRIMAL GRAMMAR inference rule constructs a primal grammar from a supposed divergent sequence, and it generates new lemmas which will subsume all divergent sequences. Procedure REMOVELIST(T, E ) removes any subgoal in T subsumed by a lemma in E . Procedure PRIMGRAM(T) returns a new primal grammar G with a new signature S and new lemmas E . If PRIMGRAM(T) fails, it returns the tuple ( , , ). The SUCCESS inference rule will be applied if the set of conjectures is exhausted. The inference rule DISPROOF applies if no other rule can be applied to c. The flag B prevents the PRIMAL GRAMMAR inference rule to be applied in an infinite loop. The diagram in Figure 2 presents the strategy for applying the inference rules. SIMPLIFY means that the simplification rule is used exhaustively until no further simplifications can take place. Given a set of conjectures, we start with the saturation of the application of the SIMPLIFY inference rule; if the resulting set of conjectures is exhausted, the SUCCESS inference rule is applied, confirming the validity of the conjectures in the initial model of R. If the SIMPLIFY process does not exhaust the conjectures, we try to apply the INDUCTIVE NARROWING inference rule. If the application of INDUCTIVE NARROWING fails, we conclude that at least one of the conjectures is not valid in the initial model. Alternatively, if the INDUCTIVE NARROWING rule succeeds, we move to the simplification step. If, once again, the resulting set of conjectures is exhausted, the SUCCESS inference rule will be applied. However, if the simplification process does not exhaust the conjectures, we apply the PRIMAL GRAMMAR inference rule.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

INIT: (E, , , [], , false)

SIMPLIFY: (E {c}, H, G, T, S, B) (E E , H, G, T, S, B) if E = simplification(c, R, H, E, G)

INDUCTIVE NARROWING: (E {c}, H, G, T, S, B) (E E , H {c}, G, c :: T, S, true) where E = S σ simplification(cσ, R, H, E, G) and σ is a test substitution of c if c has an induction variable

PRIMAL GRAMMAR: (E, H, G, T, S, true) (E E , H, G G , T , S S , false) where (G , S , E ) = PRIMGRAM(T) and T = REMOVELIST(E , T)

SUCCESS: ( , H, G, T, S, B) success

DISPROOF: (E {c}, H, G, T, S, B) disproof if no other rule applies to c

Figure 1: Inference system I

If the application of the PRIMAL GRAMMAR rule succeeds, we generate new lemmas, add them to the set of conjectures, and repeat the process. If PRIMAL GRAMMAR fails, we iterate the process with the current set of conjectures.

Figure 2: Strategy for applying inference rules

Proposition 13. Let E = {c0, c1, c2, . . .} be a primitive recursive set of clauses produced by the inference system I. The sufficient length p of a prefix Ep = {c0, . . . , cp 1} to produce a primal grammar GE schematizing E is 3.

Remark. The inference process can generate multiple independent divergent sequences. In Proposition 13, the length p of a prefix Ep is, of course, associated with the length of the dependent divergent sequence {c0, . . . , cp 1}. We always consider fair derivations in this paper. Fairness roughly means that every clause in the set of conjectures E will be eventually modified by some inference rule. More formally, a derivation (E0, H0, ) (E1, H1, ) is fair if either it ends by the application of DISPROOF or the set of persisting clauses (S i T j i Ej) is empty. Our inference system I is sound and refutationally complete.

Theorem 14 (Soudness). Let R be a ground convergent rewrite system and let (E0, , , [], , false) (E1, H1, G1, T1, S1, B1) be a fair derivation that does not end by the application of DISPROOF. Then the conjectures in E are valid in the initial model of R.

Theorem 15 (Refutational Completeness). Let R be a ground convergent rewrite system which is strongly complete over free constructors. If R |= E, then all fair derivations issued from (E, , , [], , false) terminate by the application of DISPROOF.

8 Computer Experiments

Our method has been implemented in C++ with over 6000 lines of code and successfully proved automatically over fifty complex examples, including all the examples given in [Walsh, 1996], together with those left unresolved in that paper. These examples are the cornerstone for measuring the performance of a system dealing with divergent inductive proofs. These examples cannot be proved automatically with well-known theorem provers (e.g., ACL2, Isabelle, PVS, SPIKE, RRL, LEAN, Vampire) and related methods for handling divergence in proofs by induction. The systems performance of our prototype is highly dependent on the efficiency of the Primal Grammar part. In cases where only one divergent sequence is encountered for each application of Primal Grammar, the running time is always below 10ms, and usually around 5ms. If multiple divergent sequences are encountered simultaneously, the execution time may vary from 0.045s to 18.645s. A fairly complex example proving the correctness of insert sort, with numerous divergent sequences, requires 207 proof cycles (according to Figure 2), produces 33 lemmas, and runs in 6.05 seconds. The example taking the longest time, proving (x y)z = xz yz, requires 56 proof cycles and runs in 18.645s. The mean execution time of all the examples is 0.62s and the standard deviation is 2.74s. All times are measured on a Dell Precision 3630 Tower with Intel Core i7-9700 8 processor and 16GB memory, running under Fedora Linux 39. These examples can be found at the github page https://github.com/Bouhoula Hermann/IJCAI-2024. Let us now observe how an inductive proof proceeds when it needs to construct and use primal grammars.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

Example 16. Consider the rewrite system

x + 0 x; x + s(y) s(x + y); x 0 0; x s(y) (x y) + x.

of natural numbers with addition + and multiplication , and the conjecture s(x) y = y +(x y). Despite the very simple specification, this proof triggers considerable complications with a tripple divergence and cannot be proved by other theorem provers. Only y is an induction variable in the conjecture. Its test set is composed of the terms 0 and s(x). The instantiation of y by 0 leads to a tautology. The inference system encounters first the divergent sequence of equations

s((y + (x y)) + x) = s(y) + ((x y) + x), s((s(y) + ((x y) + x)) + x) = s2(y) + (((x y) + x) + x), s((s2(y) + (((x y) + x) + x)) + x) = s3(y) + ((((x y) + x) + x) + x)

out of which it constructs a primal grammar with the Presburger system

ˆf0(0; y) y, ˆf0(n0 + 1; y) s( ˆf0(n0; y)), ˆf1(0; x, y) x y, ˆf1(n1 + 1; x, y) ˆf1(n1; x, y) + x

and the lemma

s(( ˆf0(n; y) + ˆf1(n; x, y)) + x) = s( ˆf0(n; y)) + ( ˆf1(n; x, y) + x).

This lemma is then used to subsume the clause s((s3(y) + ((((x y) + x) + x) + x)) + x) = s4(y) + (((((x y) + x) + x) + x) + x).

modulo the Presburger rewrite system using the counter substitution n 3. The inference system encounters then another divergent sequence of equations

s(s2(0 + y) + y) = s2(0) + (s(0 + y) + y)

s(s3(0 + y) + y) = s2(0) + (s2(0 + y) + y)

s(s4(0 + y) + y) = s2(0) + (s3(0 + y) + y)

out of which it constructs a primal grammar with the Presburger system

ˆf3(0; y) 0 + y, ˆf3(n + 1; y) s( ˆf3(n; y))

and the lemma

s(s2( ˆf3(n; y)) + y) = s2(0) + (s( ˆf3(n; y)) + y).

This lemma is then used to subsume the clause

s(s5(0 + y) + y) = s2(0) + (s4(0 + y) + y)

with the counter substitution n 3. The inference system encounters yet another divergent sequence of equations

s(s(s2(0) + (s(0 + y) + y)) + y) = s3(0) + ((s2(0) + ((0 + y) + y)) + y), s(s2(s2(0) + (s2(0 + y) + y)) + y) = s3(0) + (s(s2(0) + (s(0 + y) + y)) + y), s(s3(s2(0) + (s3(0 + y) + y)) + y) = s3(0) + (s2(s2(0) + (s2(0 + y) + y)) + y),

out of which it constructs a primal grammar with the Presburger system

ˆf4(0, k; y) s2(0) + (s( ˆf3(k; y)) + y), ˆf4(n + 1, k; y) s( ˆf4(n, k + 1; y)), ˆf5(0, k; y) s2(0) + ( ˆf3(k; y) + y), ˆf5(n + 1, k; y) s( ˆf5(n, k + 1; y)),

and the lemma

s(s( ˆf4(n, 0; y)) + y) = s3(0) + ( ˆf5(n, 0; y) + y).

This lemma is then used to subsume the clause

s(s4(s2(0) + (s(s3(0 + y)) + y)) + y) = s3(0) + (s3(s2(0) + (s3(0 + y) + y)) + y)

with the counter substitution n 3. After this third subsumption there remain no conjectures in the inference system and the proof terminates with success. Similarly, if we try to prove the conjecture s(x) + x = s(x + x), the proof diverges and our system produces, after four cycles, a primal grammar with the Presburger system

ˆf0(0; x) x, ˆf0(n0 + 1; x) s( ˆf0(n0; x)), ˆf1(0; x) x + x, ˆf1(n1 + 1; x) s( ˆf1(n1; x)),

and the lemma s(s( ˆf0(n; x))) + x = s(s( ˆf1(n; x))) that allows breaking the divergence and finishing the proof. Note that there is no solution in [Walsh, 1996] for finishing the proof of the first conjecture and two supplementary lemmas are necessary to prove the second one.

9 Concluding Remarks We presented a new method that allows to perform inductive proofs in conditional theories which automatically detects divergence of proof traces and derives primal grammars together with new lemmas that schematize the divergent sequences and thus, allow breaking the divergence and finishing the proof. The main advantages of our method compared to previous methods are: (i) it is completely automatic, i.e., no interaction with the user, (ii) it preserves refutational completeness. Refutational completeness is particularly useful for detecting flaws in critical systems, and (iii) there is no risk of over-generalization. Our method has been implemented in C++ and successfully proved several dozens of complex examples that fail with well-known theorem provers and related methods for capturing and schematizing divergence for proof by induction. This research represents a significant advancement in automated reasoning as it can be integrated with existing automated and interactive proof systems to improve their performance. Moreover, computer experiments show that our method is very promising and can significantly reduce the time needed to verify critical systems. We plan to generalize our method to automated theorem proving in membership equational logic [Bouhoula et al., 2000; Bouhoula and Jouannaud, 2001], as well as in higherorder logic [Nipkow et al., 2002].

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

[Aubin, 1976] Raymond Aubin. Mechanizing structural induction. Ph D thesis, University of Edinburgh, UK, 1976. [Baader and Nipkow, 1998] Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. [Basin and Walsh, 1992] David A. Basin and Toby Walsh. Difference matching. In D. Kapur, editor, Proceedings 11th International Conference on Automated Deduction (CADE 1992), Saratoga Springs (New York, USA), volume 607 of Lecture Notes in Computer Science, pages 295 309. Springer, June 1992. [Basin and Walsh, 1993] David A. Basin and Toby Walsh. Difference unification. In Ruˇzena Bajcsy, editor, Proceedings 13th International Joint Conference on Artificial Intelligence (IJCAI 1993), Chamb ery (France), pages 116 122. Morgan Kaufmann, 1993. [Bouhoula and Jouannaud, 1997] Adel Bouhoula and Jean Pierre Jouannaud. Automata-driven automated induction. In Proceedings 12th Annual IEEE Symposium on Logic in Computer Science (LICS 1997), Warsaw (Poland), pages 14 25. IEEE Computer Society, 1997. [Bouhoula and Jouannaud, 2001] Adel Bouhoula and Jean Pierre Jouannaud. Automata-driven automated induction. Information and Computation, 169(1):1 22, 2001. A preliminary version was published in [Bouhoula and Jouannaud, 1997]. [Bouhoula and Rusinowitch, 1993] Adel Bouhoula and Micha el Rusinowitch. Automatic case analysis in proof by induction. In Ruˇzena Bajcsy, editor, Proceedings 13th International Joint Conference on Artificial Intelligence (IJCAI 1993), Chamb ery (France), pages 88 -94. Morgan Kaufmann, 1993. [Bouhoula et al., 1995] Adel Bouhoula, Emmanuel Kounalis, and Micha el Rusinowitch. Automated mathematical induction. Journal of Logic and Computation, 5(5):631 668, 1995. [Bouhoula et al., 2000] Adel Bouhoula, Jean-Pierre Jouannaud, and Jos e Meseguer. Specification and proof in membership equational logic. Theoretical Computer Science, 236(1-2):35 132, 2000. [Bouhoula, 1997] Adel Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47 77, 1997. [Bouhoula, 2000] Adel Bouhoula. Simultaneous checking of completeness and ground confluence. In Proceedings 15th IEEE International Conference on Automated Software Engineering, (ASE 2000), Grenoble (France), pages 143 151. IEEE Computer Society, 2000. [Bouhoula, 2009] Adel Bouhoula. Simultaneous checking of completeness and ground confluence for algebraic specifications. ACM Transactions on Computational Logic, 10(3):20:1 20:33, 2009. A preliminary version was published in [Bouhoula, 2000].

[Boyer and Moore, 1979] Robert S. Boyer and J Strother Moore. A computational logic handbook, volume 23 of Perspectives in computing. Academic Press, 1979. [Bundy et al., 1993] Alan Bundy, Andrew Stevens, Frank van Harmelen, Andrew Ireland, and Alan Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62(2):185 253, 1993. [Chen et al., 1990] Hong Chen, Jieh Hsiang, and Hwa Chung Kong. On finite representations of infinite sequences of terms. In St ephane Kaplan and Mitsuhiro Okada, editors, Proceedings 2nd International Workshop on Conditional and Typed Rewriting Systems (CTRS 1990), Montreal (Canada), volume 516 of Lecture Notes in Computer Science, pages 100 114. Springer, 1990. [Comon, 1995] Hubert Comon. On unification of terms with integer exponents. Mathematical Systems Theory, 28(1):67 88, 1995. [de Moura and Ullrich, 2021] Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Andr e Platzer and Geoff Sutcliffe, editors, Proceedings 28th International Conference on Automated Deduction (CADE 2021), Virtual Event, volume 12699 of Lecture Notes in Computer Science, pages 625 635. Springer, 2021. [Dershowitz and Jouannaud, 1991] Nachum Dershowitz and Jean-Pierre Jouannaud. Notations for rewting. Bulletin of EATCS, 43:162 174, 1991. [Hajd u et al., 2020] M arton Hajd u, Petra Hozzov a, Laura Kov acs, Johannes Schoisswohl, and Andrei Voronkov. Induction with generalization in superposition reasoning. In Christoph Benzm uller and Bruce R. Miller, editors, Proceedings 13th International Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro (Italy), volume 12236 of Lecture Notes in Computer Science, pages 123 137. Springer, 2020. [Hermann and Galbav y, 1997] Miki Hermann and Roman Galbav y. Unification of infinite sets of terms schematized by primal grammars. Theoretical Computer Science, 176(1-2):111 158, 1997. [Hozzov a et al., 2021] Petra Hozzov a, Laura Kov acs, and Andrei Voronkov. Integer induction in saturation. In Andr e Platzer and Geoff Sutcliffe, editors, Proceedings 28th International Conference on Automated Deduction (CADE 2021), Virtual Event, volume 12699 of Lecture Notes in Computer Science, pages 361 377. Springer, 2021. [Ireland and Bundy, 1996] Andrew Ireland and Alan Bundy. Extensions to a generalization critic for inductive proof. In Michael A. Mc Robbie and John K. Slaney, editors, Proceedings 13th International Conference on Automated Deduction (CADE-13), New Brunswick (New Jersey, USA), volume 1104 of Lecture Notes in Computer Science, pages 47 61. Springer, 1996. [Kapur and Subramaniam, 1996] Deepak Kapur and Mahadevan Subramaniam. Lemma discovery in automated induction. In Michael A. Mc Robbie and John K. Slaney,

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)

editors, Proceedings 13th International Conference on Automated Deduction (CADE-13), New Brunswick (New Jersey, USA), volume 1104 of Lecture Notes in Computer Science, pages 538 552. Springer, 1996. [Kapur and Zhang, 1995] Deepak Kapur and Hantao Zhang. An overview of rewrite rule laboratory (RRL). Computers & Mathematics with Applications, 29(2):91 114, 1995. [Kaufmann et al., 2000] Matt Kaufmann, Panagiotis Manolios, and J. Strother Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, June 2000. [Nipkow et al., 2002] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. [Rushby et al., 1998] John M. Rushby, Sam Owre, and Natarajan Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709 720, 1998. [Salzer, 1992] Gernot Salzer. The unification of infinite sets of terms and its applications. In Andrei Voronkov, editor, Proceedings 3rd International Conference on Logic Programming and Automated Reasoning (LPAR 1992), St. Petersburg (Russia), volume 624 of Lecture Notes in Computer Science, pages 409 420. Springer, 1992. [Urso and Kounalis, 2004] Pascal Urso and Emmanuel Kounalis. Sound generalizations in mathematical induction. Theoretical Computer Science, 323(1-3):443 471, 2004. [Walsh, 1996] Toby Walsh. Divergence critic for inductive proofs. Journal of Artificial Intelligence Research, 4:209 235, 1996.

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24)