On Notions of Inductive Validity for First-Order Equational Clauses^{⋆}

Claus-Peter Wirth and Bernhard Gramlich

Universität Kaiserslautern, D-67663 Kaiserslautern, Germany

            {wirth,gramlich}@informatik.uni-kl.de

Abstract. We define and discuss various conceivable notions of inductive validity for first-order equational clauses. This is done within the framework of constructor-based positive/negative conditional equational specifications which permits to treat negation and incomplete function definitions in an adequate and natural fashion. Moreover, we show that under some reasonable assumptions all these notions are monotonic w. r. t. consistent extension, in contrast to the case of inductive validity for initial semantics (of unconditional or positive conditional equations). In particular from a practical point of view, this monotonicity property is crucial since it allows for an incremental construction process of complex specifications where consistent extensions of specifications cannot destroy the validity of (already proved) inductive properties. Finally we show how various notions of inductive validity in the literature fit in or are related to our classification.

1 Introduction, Motivation, and Overview

Given some finite axiomatization R, e. g., by means of a set of equations or — more generally — of first-order formulas, one is often not only interested in those properties that are logical consequences of R, i. e. that hold in all models of R but also in properties that only hold in some specific intended model (or class of models) specified by R. Instead of restricting the class of models by some required property, one may also define notions of validity by saying that a formula P (x) is to hold schematically in the sense that it is to hold for certain sets of instantiations for the variables x of P (x).

Concerning the adequacy of a notion of inductive validity we think that there are at least three important criteria.

Coincidence with intuition: It should capture the intention of the human

specifier as close as possible. Monotonicity behaviour: Whenever we extend a specification in some con-

sistent manner then previously valid formulas should still be valid w. r. t. the extended specification.

⋆ This research was supported by “Deutsche Forschungsgemeinschaft, SFB 314 (D4)”.

Operational feasibility: It should be operationally feasible in the sense that there are operational characterizations or at least sufficient operational criteria which provide the basis for corresponding theorem proving techniques.

For specifications with unconditional (or positive conditional) equations it is well-known how to obtain initial semantics and how to prove inductive theorems, i. e. equations that hold in the initial model (cf. e. g. [Bac88]). Consider for instance the following specification R over the natural numbers where addition (+) is defined in terms of zero (0) and successor (s).

R : 0 + y = y , s(x) + y = s(x + y) .

Here it is easy to show by standard techniques (cf. e. g. [BM79], [Bac88]) that

x + 0 = x

is an inductive theorem, i. e. holds in the initial model. If we now enrich the above specification by a subtraction operation (−) with

x − 0 = x , s(x) − s(y) = x − y ,

yielding a new specification R′, then, unfortunately, x + 0 = x is no longer inductively valid in the enriched specification (to wit, substitute 0 − s(0) for x). Hence, initial semantics does not enjoy the above-mentioned monotonicity property w. r. t. consistent extension. The intuitive reason for that phenomenon is that by enriching our basic specification R as described above we have introduced new junk terms which should not be considered for verification purposes. This intention will be formally reflected in our approach by distinguishing between constructor and general variables which permits to refine the class of (ground) instances of a theorem that we would like to hold.

Another crucial problem with initial semantics has to do with the way that negative statements are interpreted. For instance, the negative equation

0 − s(0) ≠ 0

holds in the initial model of R′. But if we now complete the partial definition of subtraction in some consistent manner, e. g., by adding

0 − s(y) = 0

yielding the new specification R′′, then 0 − s(0) ≠ 0 does not hold any more in the initial model of R′′. Of course, also validity of conditional statements or general first-order clauses is influenced by this phenomenon. One may argue now that in R′ we are not yet sure whether 0 − s(0) ≠ 0 is to hold because it depends on the way we might (consistently) complete the definition of ‘−’ later on in the specification process. Thus, the existence of negative literals in formulas to be proved opens up — or even necessarily entails — various ways of defining inductive validity, in particular if we want to guarantee some reasonable monotonicity property w. r. t. consistent extension. Pioneering papers along this line of reasoning are [KM87] and [KM86] (cf. also [Zha88], [ZKK88]). But whereas in these papers the specifications treated are systems of unconditional equations, and the formulas considered are pure equations, here we shall permit general equational first-order clauses as formulas and, moreover, as specifications we admit positive/negative conditional equational systems which naturally arise in many cases.

Before going into details, let us give a rough idea of our underlying specification formalism using constructor-based positive/negative conditional equations. The basic characteristics of our approach (as developed in [WG93]) may be summarized as follows: The set of function symbols is partitioned into constructor and non-constructor function symbols. The non-constructor function symbols can be used for (possibly partially) defining functions on a domain of discourse supplied by the constructor (ground) terms and called the constructor sub-universe. For such partial definitions of functions, variables ranging only over the constructor terms are useful because sometimes the specifier does not want to prescribe how the functions have to behave on objects that are undefined in the sense that they do not belong to the domain of discourse. Therefore, in addition to the usual general variables we also permit constructor variables. As axiomatizations we consider sets of positive/negative conditional equations of the form ⋀_{i=1}^{m}(s_{i} = t_{i}) ∧ ⋀_{j=1}^{n}(u_{j} ≠ v_{j}) ⇒ l = r . In general, specifications with such positive/negative conditional equations lack a unique minimal (i. e. an initial) model. In [Kap87] an operational semantics is developed which — under some reasonable assumptions — distinguishes one of the minimal models by extracting control information from the equations (considered as rewrite rules). In contrast to [Kap87] we use two syntactically expressible restrictions on the form of the equations/rules in order to obtain an appropriate semantics: Namely, the terms in the negative conditions must be defined and the constructor rules are required to have Horn-form and to be constructor-preserving (see below). For such positive/negative conditional rule systems a reduction relation can be defined which is monotonic w. r. t. consistent extension and which provides an operational characterization of a unique minimal model.

As formulas to be proved we consider (implicitly universally quantified) first-order clauses of the form A_{1} ∧ … ∧ A_{m} ⟶ B_{1} ∨ … ∨ B_{n} where the A_{i}’s and the B_{j}’s are atoms over the predicate symbols ‘=’ (equality) and ‘Def ’ (definedness predicate) on terms (with general and constructor variables). Some interesting types of inductive validity of such formulas w. r. t. a positive/negative conditional rule system R are defined by restricting the class of models to be considered. Other interesting types of inductive validity are defined by means of inductive substitutions, i. e., substitutions that substitute constructor ground terms for constructor variables and leave general variables invariant. The latter invariance for general variables corresponds to the intuition that general variables should be permitted to range not only over the junk generated by general ground terms but also over additional junk, e. g., of non-constructor symbols which might be introduced later on. Indeed, permitting this additional junk is necessary for the intended monotonicity of the notions of inductive validity w. r. t. consistent extension of the specification.

A more detailed discussion of the subject (as well as missing proofs which we have to omit here due to lack of space) can be found in [WGKP93].

2 Preliminaries

2.1 Basic Notions and Notations

We assume familiarity with the basic notions and notations for syntax and semantics of (conditional) term rewriting systems (cf. e. g. [DJ90]). Due to lack of space and for the sake of readability we restrict our presentation to the onesorted case (cf. [WGKP93] for the more general many-sorted case). We will consider terms over a signature sig = (𝔽, α) with sub-signature cons = (ℂ, α|_{ℂ}) where the functions symbols from ℂ ⊆ 𝔽 are constructor and those of 𝔽 \ ℂ are non-constructor function symbols, and where α denotes the corresponding arity function (all symbols are assumed to have fixed arity). We consider two distinct types of variables corresponding to their intended usage later on. Namely, V_{SIG} and V_{CONS} denote the set of general variables and of constructor variables, respectively. The set V of all variables is given by V := V_{SIG} ⊎ V_{CONS}. T_{SIG} := T (sig, V_{SIG}⊎V_{CONS}) is the set of (variable-mixed) general terms, T_{CONS} := T (cons, V_{CONS}) the set of pure constructor terms, and T (cons, V_{SIG}⊎V_{CONS}) the set of (variable-mixed) constructor terms. GT (cons) := T (cons, ∅) denotes the set of all constructor ground terms and GT (sig) := T (sig, ∅) the set of all ground terms. To avoid problems with empty domains we assume that GT (cons) is non-empty. In order to avoid confusion note that we have T_{CONS} ⊆ T_{SIG} but V_{CONS} ∩ V_{SIG} = ∅. Furthermore, for X = X_{CONS} ⊎ X_{SIG}, X_{CONS} ⊆ V_{CONS}, X_{SIG} ⊆ V_{SIG}, and some set T = T_{CONS} ∪ T_{SIG} we define SUB(X, T) := {σ : X → T | ∀ζ ∈ {SIG, CONS} : ∀x ∈ X_{ζ} : σ(x) ∈ T_{ζ}}. For a term t, we shall use postfix-notation tσ instead of σ(t).

Instead of the usual sig-algebras we deal with sig/cons-algebras with universe A(SIG) and constructor sub-universe A(CONS) ⊆ A(SIG) which are defined as usual except for the requirement c^{A}[A(CONS)× … ×A(CONS)] ⊆ A(CONS) (for c ∈ ℂ). A sig/cons-homomorphism h : A ⟶ B is a usual sighomomorphism with the additional requirement h[A(CONS)] ⊆ B(CONS). For X ⊆ V we use T (X) to denote the term algebra over X and sig/cons/V (where T (X)(SIG) := T (sig, X) ∩ T_{SIG} and T (X)(CONS) := T (sig, X) ∩ T_{CONS}). For a sig/cons-algebra A and a sig-congruence ∼ on A(SIG), the factor algebra B of A modulo ∼ (denoted by A/∼) is given by B(CONS) := { ∼ [{a}] | a ∈ A(CONS) } with B(SIG) and f^{B} as usual (here, ∼ [{a}] denotes the ∼-congruence class of a). For a sig/cons-algebra A, an A-valuation κ of X is an element of SUB(X, A). For DUNNO ∈ {SIG, CONS}, dunno ∈ {sig, cons} a sig/cons-algebra A is called DUNNO:dunno-term-generated if the following holds: ∀a ∈ A(DUNNO) : ∃t ∈ GT (dunno) : A(t) = a. A is called dunno-term-generated if it is SIG:dunno-term-generated. For K a class of sig/cons-algebras, A a sig/cons-algebra, X ⊆ V and κ ∈ SUB(X, A) we need the following definitions: A is initial in K if A ∈ K and for all B ∈ K there is a unique h : A → B. A is free for K over X w. r. t. κ if for all B ∈ K and μ ∈ SUB(X, B) there is a unique h : A → B with μ = κh. A is free in K over X w. r. t. κ if A ∈ K and A is free for K over X w. r. t. κ.

Note that our notion of sig/cons-algebras can be viewed as a very special (and simple) case of order-sorted structures, e. g., in the sense of [SNGM89].

2.2 Constructor-Based Positive/Negative Conditional Equational Specifications

Definition 1. (Positive/Negative Conditional Term Rewriting System) A positive/negative conditional term rewriting system (PNCTRS for short) over sig/cons/V is a set of rules^{2} of the form

⋀_{i=1}^{m}(s_{i} = t_{i}) ∧ ⋀_{j=1}^{n}(u_{j} ≠ v_{j}) ∧ ⋀_{k=1}^{p}(Def w_{k}) ⇒ l = r

with all s_{i}, t_{i}, u_{j}, v_{j}, w_{k} in T (sig, V_{SIG}⊎V_{CONS}).

Definition 2. (Semantics of PNCTRSs) If R is a PNCTRS over sig/cons/V then a sig/cons-algebra A is said to be a model of R if we have: ∀(P ⇒ l=r) ∈ R: ∀κ ∈ SUB(V, A): ((P is true w.r.t. A_{κ}) ⇒ A_{κ}(l) = A_{κ}(r)) where P is true w. r. t. A_{κ} if all its literals are true w. r. t. A_{κ}, i. e., A_{κ}(u) = A_{κ}(v) for (u = v) in P, A_{κ}(u) ≠ A_{κ}(v) for (u ≠ v) in P, and A_{κ}(u) ∈ A(CONS) for (Def u) in P.

Definition 3. (Minimal and Minimum Model) Let the quasi-orderings ≲_{H} and ≲_{CONS} on sig/cons-algebras be defined by: A ≲_{H}B if there exists a sig/cons-homomorphism from A to B. A ≲_{CONS}B if there exists a cons-homomorphism from A|_{ℂ⊎{CONS}} to B|_{ℂ⊎{CONS}}.^{3} A sig/cons-algebra A is a minimal model of a PNCTRS R if it is minimal w. r. t. ≲_{H} in the class M of all models of R. It is a constructor-minimal model of R if it is minimal w. r. t. ≲_{CONS} in M. A is a minimum model of R if it is a least model of R w. r. t. ≲_{H}, and it is a constructor-minimum model of R if it is a least model of R w. r. t. ≲_{CONS}.

Now, every PNCTRS possesses minimal models, but not necessarily a minimum model. But as we shall see, under certain restrictions we are able to guarantee the existence of a constructor-minimum model which can be constructed as a quotient term algebra. To this end we have to define a reduction relation for PNCTRSs. This is only possible in a reasonable way — without assuming some termination ordering conditions as in [Kap87] — by imposing additional restrictions on the structure of the rules. To be precise, we require for every constructor rule of R, i. e., for every (P ⇒ l=r) ∈ R with l ∈ T (cons, V_{SIG}⊎V_{CONS}):

2 We shall always use ‘=’ in equations or rules. The interpretation as ‘=’ or ‘→’ tacitly

depends on the context. 3 By the notation A|_{ℂ⊎{CONS}} we mean the cons-algebra of A with universe A(CONS).

(1) There are no negative equations in P (constructor rules have “Horn”-form), and

(2) All terms in r and P are constructor terms, i. e., in T (cons, V_{SIG}⊎V_{CONS}), and all variables of r and P occur in l (“constructor-preservation”).

PNCTRSs satisfying these conditions are called constructor-based. In the rest of the paper all PNCTRSs are tacitly assumed to be constructor-based.

Now we are prepared to define the reduction relation.

Definition 4. (Reduction Relation) Let R be a (constructor-based) PNCTRS over sig/cons/V and R_{ℂ} its subset of constructor rules.^{4} For X ⊆ V the reduction relation →_{R,X} on T (sig, X) induced by R is the smallest relation → satisfying → ∩ (GT (cons) × T_{SIG}) ⊆→_{R_{ℂ},X},^{5} and s → t if s, t ∈ T (sig, X) and

∃(P ⇒ l=r) ∈ R: ∃σ ∈ SUB(V, T (X)): ∃p ∈ POS(s): ( \begin{matrix}s/p = lσ ∧ \\ t = s[p ← rσ] ∧ \\ P σ fulfilled w.r.t. → \end{matrix} )

where “Q is fulfilled w. r. t. →” is a shorthand for

∀(u = v) in Q : u ↓ v
∧ ∀(Def u) in Q : ∃û ∈ GT (cons) : u →^{∗} û
∧ ∀(u ≠ v) in Q : ∃û, v̂ ∈ GT (cons) : u →^{∗} û∤ ↓v̂ ←^{∗} v

The well-definedness of →_{R,X} can be established by a double closure construction, firstly for the constructor rules only (which is possible due to their required Horn-form), and secondly for general rules knowing that the reduction relation on constructor ground terms remains invariant (due to the required constructorpreservation property).

Note moreover that →_{R,X} is stable under substitutions from SUB(V, T (X)). Furthermore, for X ⊆ Y, confluence of →_{R,Y} implies confluence of →_{R,X}.

In order to guarantee the existence of a constructor-minimum model of R we have to require that the reduction relation is (ground) confluent^{6} and that the terms of the negative equations in the conditions of R are “defined”.

Definition 5. (Def-Moderate PNCTRS) A (constructor-based) PNCTRS is called Def-moderate (Def-MCTRS for short) if for each rule (P ⇒ l=r) ∈ R and each negative condition (u ≠ v) in P we have that (Def u), (Def v) are in P, too.

Theorem 6.(Existence and Characterization of a Constructor-Minimum Model) Let R be a Def-MCTRS over sig/cons/V and K be the class of all constructorminimal models of R. Moreover, let X ⊆ V and κ be given by: x ↦ ↔_{R,X}^{∗} [{x}]. Then the following holds:

4 i. e., R_{ℂ} is a positive conditional system consisting of those rules of R that do not

involve non-constructor function symbols. 5 This requirement ensures minimality of → on the constructor (ground) terms. 6 Although many of our results do not depend on the (ground) confluence assump-

tion, this property is desirable anyway, since otherwise, for instance the congruence induced by the reduction relation of some R need not yield a model of R in general.

• If →_{R,∅} is confluent then T (X)/↔_{R,X}^{∗} is free for K over X w. r. t. κ.

• If →_{R,X} is confluent and X ⊆ V_{SIG}, then T (X)/↔_{R,X}^{∗} is a minimal model of R which is free in K over X w. r. t. κ and which is moreover a constructorminimum model of R.

Corollary 7. If R is a Def-MCTRS such that →_{R,∅} is confluent then GT /↔_{R,∅}^{∗} is a minimal model of R which is initial in the class of all constructor-minimal models of R and which is the (up to isomorphism) unique ≲_{H}-minimum of all sig-term-generated constructor-minimal models of R.

Hence, for confluent →_{R,∅} the factor algebra GT /↔_{R,∅}^{∗} provides us with a constructive operational characterization of the intended unique minimal model. Moreover, the reduction relation is monotonic w. r. t. consistent extension in the following sense.

Theorem 8. (Monotonicity of →_{R,X} w. r. t. Consistent Extension)

Let R be a PNCTRS over sig/cons/V and let R′ be another PNCTRS over

sig′/cons′/V′ with  sig′ = (𝔽′, α′)  𝔽 ⊆ 𝔽′  R ⊆ R′ cons′ = (ℂ′, α′|_{ℂ′}) ℂ = ℂ′ X ⊆ X′ V′ = V  α ⊆ α′ .

Moreover assume that no new (i. e., of a rule from R′ \ R) left-hand side is a constructor term. Then the following properties hold:

• The reduction relations →_{R,X} and →_{R′,X′} coincide for constructor terms, i. e.: ∀s ∈ T (cons, X) : ∀t : (s →_{R′,X′}^{∗} t ⇔ s →_{R,X}^{∗} t ⇔ s →_{R_{ℂ},X}^{∗} t).

• The reduction relation →_{R,X} is monotonic in X and R: →_{R,X} ⊆ →_{R′,X′}.

In [WG93] we have developed a couple of confluence criteria for PNCTRSs as well as some slightly extended “decreasingness”-notions which generalize known results for positive conditional rewrite systems (e. g., of [DOS88]). For related work on PNCTRSs see also [AB92], [Bec93].

3 Inductive Validity: Notions and Interrelations

Definition 9. (Syntax of Formulas) Let X ⊆ V. The set of formulas (or Gentzen clauses) over sig, X is defined to be FORM(sig, X) := ATOM(sig, X)^{∗} ×ATOM(sig, X)^{∗}, where ATOM(sig, X) is the set of atoms over the predicate symbols ‘=’ and ‘Def ’ on terms from T (sig, X). A formula (Γ, Δ) will also be denoted by Γ ⟶Δ. For the special cases of ⟶Δ and (s = t) ⟶ we also write Δ and (s ≠ t) , respectively.

Definition 10. (Validity of Formulas in Algebras) Let X ⊆ V, A be a sig/cons-algebra, and κ ∈ SUB(X, A). An atom (u = v) ∈ ATOM(sig, X) is true w. r. t. A_{κ} if A_{κ}(u) = A_{κ}(v). An atom (Def u) ∈ ATOM(sig, X) is true w. r. t. A_{κ} if A_{κ}(u) ∈ A(CONS). A formula (Γ ⟶Δ) ∈ FORM(sig, X) is valid in A if ∀κ ∈ SUB(X, A):

(∀A in Γ: (A is true w. r. t. A_{κ}) ⇒ ∃B in Δ: (B is true w. r. t. A_{κ})).

Next we introduce a notion for substitutions that replace constructor variables by constructor ground terms and leave the general variables invariant.

Definition 11. (Inductive Substitutions) The set of inductive substitutions is defined by: INDSUB(V, cons) := {τ ∈ SUB(V, T (V_{SIG})) | τ[V_{CONS}] ⊆ GT (cons) ∧ τ|_{V_{SIG}}=id|_{V_{SIG}}}.

Definition 12. (Type-A / B′ / B / C / D′ / D / E Inductive Validity) Let R be a PNCTRS over sig/cons/V, let M be the class of all models of R and K be the class of all constructor-minimal models of R. Then a formula (Γ⟶Δ) ∈ FORM(sig, V) is said to be

— type-A inductively valid w. r. t. R, denoted by R ⊧_{ind}^{A} Γ ⟶Δ, if
∀A ∈ M: ∀τ ∈ INDSUB(V, cons): (Γ ⟶Δ)τ is valid in A.
— type-B′ inductively valid w. r. t. R, denoted by R ⊧_{ind}^{B′} Γ ⟶Δ, if
∀A ∈ M: ((A is CONS:cons-term-generated) ⇒ (Γ ⟶Δ) is valid in A).
— type-B inductively valid w. r. t. R, denoted by R ⊧_{ind}^{B} Γ ⟶Δ, if
∀A ∈ K: ∀τ ∈ INDSUB(V, cons): (Γ ⟶Δ)τ is valid in A.
— type-C inductively valid w. r. t. R, denoted by R ⊧_{ind}^{C} Γ ⟶Δ, if
∀A ∈ K: ((A is CONS:cons-term-generated) ⇒ (Γ ⟶Δ) is valid in A).
— type-D′ inductively valid w. r. t. R, denoted by R ⊧_{ind}^{D′} Γ ⟶Δ, if
∀A ∈ K: ((A is SIG:cons-term-generated) ⇒ (Γ ⟶Δ) is valid in A).
— type-D inductively valid w. r. t. R, denoted by R ⊧_{ind}^{D} Γ ⟶Δ, if

(Γ ⟶Δ) is valid in T (V_{SIG})/↔^{∗}_{R,V_{SIG}}.

— type-E inductively valid w. r. t. R, denoted by R ⊧_{ind}^{E} Γ ⟶Δ, if

(Γ ⟶Δ) is valid in GT /↔^{∗}_{R,∅}.

Type-A formulates the idea that (constructor) variables are meant to denote objects denoted by (constructor) ground terms. However, contrary to all other types, type-A does not restrict the models of the specification that have to be considered, but considers only instances of formulas obtained by inductive substitutions. Type-B′ forbids junk in the constructor sub-universe (i. e. the domain of interest), which makes inductive substitutions redundant. Type-B forbids unnecessary confusion in the constructor sub-universe. Type-C combines both restrictions, which is appealing if one wants to prescribe a precise and fixed knowledge on the basic objects for computation. Type-D′ corresponds to the philosophy that a partially defined function is to be interpreted as the set of all possible complete and consistent extensions. Type-D and E finally fix one specific unique minimal model which has neither junk nor confusion in the constructor sub-universe and which can be described constructively in terms of the factor algebra of the term algebra modulo the congruence induced by the reduction relation (provided the latter is confluent). Type-E uses the ground term algebra GT , which is only adequate (cf. Theorem 17 and Example 14) when no general variables occur in the formula. Therefore, Type-D uses the term algebra T (V_{SIG}) over V_{SIG}. In a sense, type-D means inductive semantics for V_{CONS} and free semantics for V_{SIG}. The notations of the types of inductive validity are motivated by the following result:

Lemma 13. (From Type-A down to Type-E) Let R be a PNCTRS over sig/cons/V and Γ ⟶Δ ∈ FORM(sig, V).

(a) If R ⊧_{ind}^{A} Γ ⟶Δ , then R ⊧_{ind}^{B} Γ ⟶Δ and R ⊧_{ind}^{B′} Γ ⟶Δ .

(b) If R ⊧_{ind}^{B} Γ ⟶Δ or R ⊧_{ind}^{B′} Γ ⟶Δ , then R ⊧_{ind}^{C} Γ ⟶Δ .

(c) If R ⊧_{ind}^{C} Γ ⟶ Δ , then R ⊧_{ind}^{D′} Γ ⟶ Δ and even R ⊧_{ind}^{D′} Γ′ ⟶Δ where Γ′ results form Γ by deleting (some) Def-atoms.

(d) If R is a Def-MCTRS, →_{R,V_{SIG}} is confluent, and R ⊧_{ind}^{C} Γ ⟶Δ , then R ⊧_{ind}^{D} Γ ⟶Δ .

(e) If R ⊧_{ind}^{D} Γ ⟶Δ , then R ⊧_{ind}^{E} Γ ⟶Δ .

(f) If R is a Def-MCTRS, →_{R,∅} is confluent, and R ⊧_{ind}^{C} Γ ⟶ Δ , then R ⊧_{ind}^{E} Γ ⟶Δ .

(g) Under the restrictive condition of sufficient completeness of →_{R,∅} (i. e.: ∀s ∈ GT (sig): ∃t ∈ GT (cons): s →_{R,∅}^{∗} t) the following holds: If R is a Def-MCTRS and →_{R,∅} is confluent, then we get: R ⊧_{ind}^{D′} Γ ⟶Δ ⇔ R ⊧_{ind}^{E} Γ ⟶Δ .

The basic characteristics of and the relations between these notions of inductive validity are illustrated in Figure 1 below where implications are indicated by arrows. Missing arrows indicate non-implications as shown by Example 14 below.

no confusion & no junk no confusion & and no junk for CONS, for CONS no confusion for SIG, and A(SIG) = GT (sig)/ ↔_{R,∅}^{∗} no junk for SIG, and^{A(SIG) = A[GT (cons)]} no confusion & no junk for CONS,^{A}  ^{B′}^{B}  ^{C}^{D}  ^{D′}^{E} no confusion  for CONS no junk for CONS, no confusion &^{A(SIG) = T (sig, V_{SIG})/ ↔_{R,V_{SIG}}^{∗}} no confusion for SIG, and  for CONS no junk Figure 1

Example 14. Let us return to the specification on natural numbers from section 1 and start with 𝔽 := ℂ := {s, 0} and R := ∅. Then we have

R ⊧_{ind}^{B} s(0) ≠ 0 , but R |̸=_{ind}^{A} s(0) ≠ 0 ,

since 0 and s(0) are interpreted as distinct objects in any constructor-minimal model of R, and since s(0) ≠ 0 does not hold for instance in the trivial model of R which identifies everything. Furthermore, for the same reason we have

R ⊧_{ind}^{C} s(0) ≠ 0 , but R |̸=_{ind}^{B′} s(0) ≠ 0 .

Keeping ℂ′ := ℂ, let us add two non-constructor symbols + and ω, yielding 𝔽′ := {+, ω} ⊎ ℂ, with the rules

R′: 0 + y = y, s(x) + y = s(x + y),

where it does not matter whether x, y are from V_{SIG} or V_{CONS}. Then we have

R′ ⊧_{ind}^{C} ( Def ω) ⟶ ( ω+0 = ω) , but R′ |̸=_{ind}^{B} ( Def ω) ⟶ ( ω+0 = ω) , since if (Def ω) is valid in some CONS:cons-term-generated model then ω can be denoted by some constructor ground term s^{i}(0), and since for type-B inductive validity we also have to consider (constructor-minimal) models containing constructor objects that are not denoted by some term of the form s^{i}(0), e. g. GT′/ ↔_{R′,∅}^{∗} where GT′ differs from GT only in the constructor sub-universe given as GT′(CONS) := GT (SIG). Note that GT′/↔_{R′,∅}^{∗} is constructor-minimal indeed, due to GT′/↔_{R′,∅}^{∗} ≲_{CONS} GT /↔_{R′,∅}^{∗} . Furthermore, for the same reason we have

R′ ⊧_{ind}^{B′} ( Def ω) ⟶ ( ω+0 = ω) , but R′ |̸=_{ind}^{A} ( Def ω) ⟶ ( ω+0 = ω) . Again keeping ℂ′′ := ℂ, let us add a non-constructor symbol −, yielding 𝔽′′ := {−} ⊎ ℂ, with the rules

R′′: x − 0 = x, s(x) − s(y) = x − y,

where it does not matter whether x, y are from V_{SIG} or V_{CONS}. Then we have

R′′ ⊧_{ind}^{D} 0 − s(0) ≠ 0 , but R′′ |̸=_{ind}^{D′} 0 − s(0) ≠ 0

because 0 − s(0) ≠ 0 does not hold in the SIG:cons-term-generated constructorminimal model obtained by identifying 0 − y with 0. Furthermore, R′′ ⊧_{ind}^{D′} (0 − s(0)) − (0 − s(0)) = 0 , but R′′ |̸=_{ind}^{E} (0 − s(0)) − (0 − s(0)) = 0

because a SIG:cons-term-generated model must satisfy 0 − s(0) = s^{i}(0) for some i, but (0−s(0)) − (0−s(0)) ↮_{R′′,∅}^{∗} 0 (i. e., (0−s(0)) − (0−s(0)) = 0 does not hold in the CONS:cons-term-generated, constructor-minimal model GT / ↔_{R′′,∅}^{∗} of R′′). Finally, keeping ℂ′′′ := ℂ and choosing 𝔽′′′ := {+} ⊎ ℂ, for X ∈ V_{SIG} we have R′ ⊧_{ind}^{E} X+ 0 = X (which is not the case for the consistent extension via 𝔽′′′ := 𝔽′), but R′ |̸=_{ind}^{D} X+ 0 = X, since ∀t ∈ GT (sig): t + 0 ↔_{R′,∅}^{∗} t but not X+ 0 ↔_{R′,V_{SIG}}^{∗} X .

While the example has shown that the reverse of each implication depicted in the figure does not hold in general, the following lemma gives sufficient conditions.

Lemma 15. (From Type-E up to Type-A) Let R be a PNCTRS over sig/cons/V and Γ ⟶Δ ∈ FORM(sig, V).

(a) If Γ ⟶Δ does not contain variables from V_{SIG}, then we get: R ⊧_{ind}^{E} Γ ⟶Δ ⇒ R ⊧_{ind}^{D} Γ ⟶Δ .

(b) If R is a Def-MCTRS, →_{R,∅} is confluent, and if for all (top level) terms u

of atoms in Γ we have R ⊧_{ind}^{D} (Def u), then we get: R ⊧_{ind}^{D} Γ ⟶Δ ⇒ R ⊧_{ind}^{C} Γ ⟶Δ .

(c) If for each atom (Def u) in Γ we have R ⊧_{ind}^{C} (Def u),^{7} then we get:

R ⊧_{ind}^{C} Γ ⟶Δ ⇒ R ⊧_{ind}^{B} Γ ⟶Δ . If for each atom (Def u) in Γ we have R ⊧_{ind}^{B′} (Def u),^{7} then we get:

R ⊧_{ind}^{B′} Γ ⟶Δ ⇒ R ⊧_{ind}^{A} Γ ⟶Δ .

(d) If no rule in R has a negative condition (like u ≠ v), then we get: R ⊧_{ind}^{C} Δ ⇒ R ⊧_{ind}^{A} Δ .

Note that (by Lemma 13) Lemma 15 also permits to conclude from type-C to B′ (via A), from type-B to A (via C), and from type-D′ to C (via E, D).

Lemma 16. (Operational Characterization of Type-D Inductive Validity) Let R be a PNCTRS over sig/cons/V and Γ ⟶Δ ∈ FORM(sig, V). Then R ⊧_{ind}^{D} Γ ⟶Δ is equivalent to ∀τ ∈ SUB(V, T (V_{SIG})):

∀(u=v) in Γ: uτ ↔_{R,V_{SIG}}^{∗} vτ ∧ ∀(Def u) in Γ: ∃û ∈ GT (cons): uτ ↔_{R,V_{SIG}}^{∗} û
⇒
∃(u=v) in Δ: uτ ↔_{R,V_{SIG}}^{∗} vτ ∨ ∃(Def u) in Δ: ∃û ∈ GT (cons): uτ ↔_{R,V_{SIG}}^{∗} û

Finally we show that (under some reasonable assumptions) all defined notions of inductive validity are monotonic w. r. t. consistent extension.

Theorem 17. (Monotonicity of Inductive Validity w. r. t. Consistent Extension)

Let R be a PNCTRS over sig/cons/V and let R′ be another PNCTRS over

sig′/cons′/V′ with^{8}  sig′ = (𝔽′, α′)  𝔽 ⊆ 𝔽′  R ⊆ R′ cons′ = (ℂ′, α′|_{ℂ′}) ℂ = ℂ′ X ⊆ X′ V′ = V  α ⊆ α′ .

Moreover assume that

(∗) →_{R′,∅} is confluent

and that the following condition for the new left hand sides holds:

(∗∗) ∀ (C ⇒ l=r) ∈ R′ \ R: l ∉ T (cons, V_{SIG} ⊎ V_{CONS}).

Then, for any clause Γ ⟶Δ ∈ FORM(sig, V) we have:

(A) R ⊧_{ind}^{A} Γ⟶Δ ⇒ R′ ⊧_{ind}^{A} Γ⟶Δ (even without assuming (∗), (∗∗)).
(B′) R ⊧_{ind}^{B′} Γ⟶Δ ⇒ R′ ⊧_{ind}^{B′} Γ⟶Δ (even without assuming (∗), (∗∗)).
(B) If R′ is Def-moderate then we get: R ⊧_{ind}^{B} Γ⟶Δ ⇒ R′ ⊧_{ind}^{B} Γ⟶Δ.
(C) If R′ is Def-moderate then we get: R ⊧_{ind}^{C} Γ⟶Δ ⇒ R′ ⊧_{ind}^{C} Γ⟶Δ.
(D′) If R′ is Def-moderate then we get: R ⊧_{ind}^{D′} Γ⟶Δ ⇒ R′ ⊧_{ind}^{D′} Γ⟶Δ.
(D) If for all (top level) terms u of atoms in Γ we have R ⊧_{ind}^{D} (Def u),

then we get: R ⊧_{ind}^{D} Γ⟶Δ ⇒ R′ ⊧_{ind}^{D} Γ⟶Δ.

(E) If Γ⟶Δ does not contain variables from V_{SIG},

and if for all (top level) terms u of atoms in Γ we have R ⊧_{ind}^{E} (Def u), then we get: R ⊧_{ind}^{E} Γ⟶Δ ⇒ R′ ⊧_{ind}^{E} Γ⟶Δ.

7 Even if this condition is not satisfied, the following equivalence transformation for type-B′, C, D′, D, and E validity (but not for A and B) may help to apply the Lemma : Γ, (Def u), Γ′ ⟶ Δ is equivalent to Γ, (x=u), Γ′ ⟶ Δ for a fresh (i. e. not occurring in Γ, u, Γ′, Δ) constructor variable x.

8 In a sorted framework one may even add new constructor symbols for new sorts and permit new rules with left-hand sides that are new (but not old) constructor terms.

Proof. Let A′ be some sig′/cons′-algebra. We define the sig/cons-algebra A by A := A′|_{𝔽⊎{SIG,CONS}}. Now an “old” formula Γ ⟶Δ ∈ FORM(sig, V) is valid in A if and only if it is valid in A′. Its inductive instances (Γ ⟶ Δ)τ do not differ for τ ∈ INDSUB(V, cons) and τ ∈ INDSUB(V′, cons′) due to GT (cons) = GT (cons′). Furthermore, if A′ is CONS:cons′-term-generated (or even SIG:cons′-term-generated), then A is CONS:cons-term-generated (or even SIG:cons-term-generated). Thus for proving (A), (B′ ), [and (B), (C), (D′),] it suffices to show the following claim: (∗∗∗) If A′ is a [constructor-minimal] model of R′, then A is a [constructor-minimal] model of R.

Proof of (∗∗∗): Assume that A′ is a model of R′. Then A, as defined above, is a model of R since each rule from R can be translated into an “old” formula (on which A and A′ do not differ). Let us now assume that R′ is Def-moderate and that A′ is constructor-minimal. Let GT′ and GT (cons) denote the ground term algebra over sig′/cons′ and cons, respectively. By (∗) and Theorem 6, GT′/↔_{R′,∅}^{∗} is a constructor-minimum model of R′ w. r. t. sig′/cons′. Thus, A′ must be a constructor-minimum model of R′ w. r. t. sig′/cons′, too. Hence, there exists some cons′-homomorphism h′ : A′|_{ℂ′⊎{CONS}} → (GT′/ ↔_{R′,∅}^{∗})|_{ℂ′⊎{CONS}}. By defining h(a) := h′(a) ∩ GT (cons) (for a ∈ A(CONS)), we get a conshomomorphism h : A|_{ℂ⊎{CONS}} → GT (cons)/(↔_{R′,∅}^{∗} ∩ (GT (cons)×GT (cons))). By confluence of →_{R′,∅} and Theorem 8 we get (↔_{R′,∅}^{∗} ∩ (GT (cons)×GT (cons))) ⊆ (↓_{R′,∅} ∩ (GT (cons)×GT (cons))) ⊆ ↓_{R_{ℂ},∅} ⊆ ↔_{R_{ℂ},∅}^{∗} ⊆ ker(B) for the kernel of any model B of R, and by the Homomorphism-Theorem we then get A ≲_{CONS}B. Thus, A is not only a model of R, but also a constructor-minimal one.

Proof of (D): We use the operational version of type-D inductive validity given in Lemma 16. Let τ′ ∈ SUB(V′, T′(V_{SIG}′)) and assume the condition of the implication of Lemma 16 to hold for this τ′. There exist τ ∈ INDSUB(V′, cons′) and σ ∈ SUB(V′_{SIG}, T′(V_{SIG}′)) such that τ′ = τσ and τ|_{V} ∈ SUB(V, T (V_{SIG})). By assumption we know that for each atom (u = v) in Γ the formulas (Def u) and (Def v) are valid in T (V_{SIG})/↔_{R,V_{SIG}}^{∗}. Thus there exist û, v̂ ∈ GT (cons) with uτ ↔_{R,V_{SIG}}^{∗} û and vτ ↔_{R,V_{SIG}}^{∗} v̂. By Theorem 8 we obtain uτ ↔_{R′,V_{SIG}′}^{∗} û and vτ ↔_{R′,V_{SIG}′}^{∗} v̂. Together with uτ′ ↔_{R′,V_{SIG}′}^{∗} vτ′, which holds by assumption, this yields (exploiting stability of →_{R,X}) û ↔_{R′,V_{SIG}′}^{∗} uτσ ↔_{R′,V_{SIG}′}^{∗} vτσ ↔_{R′,V_{SIG}′}^{∗} v̂. Thus (since ↔_{R,X}^{∗} ∩ (GT (cons)×GT (cons)) = ↔_{R,∅}^{∗}) we get û ↔_{R′,∅}^{∗} v̂ which, due to confluence of →_{R′,∅}, implies û ↓_{R′,∅} v̂. Theorem 8 yields û ↓_{R,∅} v̂, hence (by monotonicity of →_{R,X} in X (Theorem 8)) uτ ↔_{R,V_{SIG}}^{∗} û ↔_{R,V_{SIG}}^{∗} v̂ ↔_{R,V_{SIG}}^{∗} vτ. Furthermore, for each atom (Def u) in Γ we have assumed that (Def u) is valid in T (V_{SIG})/↔_{R,V_{SIG}}^{∗}. Thus there exists some û ∈ GT (cons) with uτ ↔_{R,V_{SIG}}^{∗} û. Because of R ⊧_{ind}^{D} Γ ⟶Δ we can conclude that there is an atom (u = v) ∈ Δ with uτ ↔_{R,V_{SIG}}^{∗} vτ or an atom (Def u) ∈ Δ with uτ ↔_{R,V_{SIG}}^{∗} û for some û ∈ GT (cons). Application of Theorem 8 yields uτ ↔_{R′,V_{SIG}′}^{∗} vτ or uτ ↔_{R′,V_{SIG}′}^{∗} û, respectively. Finally, due to τ′ = τσ (and stability of →_{R,X}) we obtain uτ′ ↔_{R′,V_{SIG}′}^{∗} vτ′ or uτ′ ↔_{R′,V_{SIG}′}^{∗} û, respectively, as desired. Summarizing, we can conclude R′ ⊧_{ind}^{D} Γ ⟶Δ as was to be shown.

Proof of (E): By Lemma 15(a), (D), Lemma 13(e).

4 Discussion and Related Work

4.1 Advantages/Disadvantages

As shown above, all our notions of inductive validity have the desired monotonic behaviour w. r. t. consistent extension (under reasonable assumptions).

Concerning operational feasibility of the different types of inductive validity, the following can be said. Type-A can be approached by usual first-order theorem proving via induction schemes relying on the fact that only the validity of the inductive instances has to be considered. For type-B, C, and D we are and will be investigating inductive theorem proving techniques which are supported by a confluent rewriting relation. Lemma 16 allows us to develop powerful inference rules for type-D, some of which are not applicable for type-C (and B), which is no surprise since less formulas are of these types. Such an approach is more powerful than presenting an inference system for type-D only and then to approach type-C (and B) via Lemma 15(b) (and (c)). To see this, consider the specification with constructor constants a, b, c and non-constructor function symbol h with partial specification h(a) = b, h(b) = a. Now the formula Def h(c) ⟶ h(h(h(c))) = h(c) is type-C valid which cannot be inferred via Lemma 15(b). It is, however, easy to show its type-C validity via a type-C equivalence transformation into x = h(c) ⟶ h(h(h(c))) = h(c) (for x ∈ V_{CONS}) and subsequent case analysis (via a “covering set” of substitutions for x) followed by “contextual rewriting”. Note that the formula h(h(h(c))) = h(c) is of type-D′ only. In fact, there are examples for type-D′ that require inferences of this kind which are far more complicated since they may not allow for a finite argumentation. Therefore, we suspect that it will be difficult to develop a prover that can effectively show those type-D′ inductively valid formulas that do not result from type-C valid formulas Γ ⟶Δ by deleting Def-atoms in Γ (cf. Lemma 13(c)).

4.2 Special Cases

In the sequel we will assume R to be a Def-MCTRS and →_{R,V_{SIG}} to be confluent.

Let us first consider the special case that cons = sig and that no variables from V_{SIG} occur in formulas. Note that, for cons = sig, our requirement of being constructor-based permits positive conditional equations only. In this case (disregarding formulas that involve Def-literals) type-A and B′ validity are validity in all ( cons = sig )-term-generated models. Furthermore, Type-B, C, D′, D, and E coincide with validity in the unique minimal term-generated model (i. e. the initial model). Hence, we obtain classic initial semantics (for positive conditional equational specifications) as a special case of our general framework.

Still not permitting general variables in formulas, another important special case is that of sufficient completeness (cf. Lemma 13(g)), where type-C, D′, D, and E again coincide, and where the model GT /↔^{∗}_{R,∅} (which establishes type-E) is cons-isomorphic to GT (cons)/↔_{R_{ℂ},∅}^{∗} (cf. Definition 4).

Let us finally restrict to positive formulas ⟶Δ. Here type-A and B′ coincide. So do B, C, and D. Furthermore, these two groups coincide when no rule in R has a negative condition (cf. Lemma 15(d)).

4.3 Related Work

Let us now have a brief look at notions of inductive validity in the literature, most of which can be described as specializations within our framework. If we consider all symbols to be constructor symbols (and, consequently, forbid negative conditions in the rules), then we find type-A in [KR90] as well as in [BKR92]. The crucial idea of requiring the values of variables in formulas to be defined, i. e., to be substituted by constructor ground terms only, seems to appear first in [Zha88], [ZKK88]. The “constructor models” of [Zha88], [ZKK88], which are not models in the usual algebraic sense since functions are allowed to be partially interpreted, are consistently formalized in our framework by introducing the simple (ordersorted) notion of sig/cons-algebras. The notion of inductive validity of [ZKK88],

[Zha88] can be described as type-A by implicitly interpreting all variables in rules as general variables and all variables in formulas as constructor variables. In [GS92] inductive validity is defined to be validity in the perfect model as introduced in [BG91]. This approach has a more general specification formalism permitting sets of first-order clauses instead of constructor-based PNCTRSs. The perfect model is determined as the least term-generated model w. r. t. some ground-total reduction ordering. The perfect model semantics, however, lacks the discussed monotonicity property. In [Pad90], [BL90], [KR88] and [BR93] we find the usual validity in the initial model which is like our type-E, assuming again all symbols to be constructor symbols and forbidding negative conditions in the rules. Kapur and Musser ([KM87], [KM86]) consider only unconditional equations and only congruences on ground terms (i. e. term-generated models) for validity, namely those that are maximally enlarged by random identification of undefined terms with defined ones (i. e. constructor ground terms) as long as this identification does not identify distinct constructor ground terms. Their intended congruence is then the intersection of all those maximally enlarged congruences. In [KM87] the maximal congruences are allowed to have some undefined terms left (accounting for the fact that the constructor-minimality requirement may forbid any further identification from some point on). The resulting “inductive models”, however, lack the discussed monotonicity property, cf. [WGKP93] for an example. Therefore, in [KM86] the intersection is formed only over those congruences that have no undefined ground terms left. While we have no notion of inductive validity corresponding to that of [KM87], inductive validity in [KM86] coincides with type-D′. Finally, the problems due to not yet known or incompletely specified function symbols are also discussed in [Wal94], mainly along the lines of [KM86].

5 Conclusion

We have shown that considering inductive validity of first-order equational clauses instead of pure unconditional equations gives rise to various conceivable notions of inductive validity. Within the framework of constructor-based positive/negative conditional equational specifications (which provides an adequate unique model semantics) we have demonstrated that all these notions enjoy a desirable monotonic behaviour w. r. t. consistent extension, which is not the case for classic initial or perfect model validity.

Acknowledgements: We would like to thank Ulrich Kühler and Horst Prote for many valuable discussions and detailed criticisms on earlier versions of this paper, Jürgen Avenhaus and Klaus Becker for fruitful discussions, and Klaus Madlener for useful hints.

References

[AB92] J. Avenhaus, K. Becker. Conditional rewriting modulo a built-in algebra. SEKI-Report SR–92–11, FB Informatik, Univ. Kaiserslautern, 1992.

[Bac88] L. Bachmair. Proof by consistency in equational theories. In Proc. 3rd IEEE Symposium on Logic in Computer Science, pp. 228–233, 1988.

[Bec93] K. Becker. Semantics for positive/negative conditional rewrite systems. In M. Rusinowitch, J.L. Rémy, eds., Proc. 3rd CTRS, LNCS 656, pp. 213–225. Springer, 1993.

[BG91] L. Bachmair, H. Ganzinger. Perfect model semantics for logic programs with equality. In Proc. 8th ICLP, pp. 645–659. MIT Press, 1991.

[BKR92] A. Bouhoula, E. Kounalis, M. Rusinowitch. Automated mathematical induction. Rapport de Recherche 1663, INRIA, April 1992.

[BL90] E. Bevers, J. Levi. Proof by consistency in conditional equational theories. In S. Kaplan, M. Okada, eds., Proc. 2nd CTRS, LNCS 516, pp. 194–205. Springer, 1990.

[BM79] R. S. Boyer, J S. Moore. A Computational Logic. Academic Press, 1979.

[BR93] A. Bouhoula, M. Rusinowitch. Automatic case analysis in proof by induction. In Proc. 13th IJCAI, pp. 88–94, 1993.

[DJ90] N. Dershowitz, J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, ed., Formal models and semantics, Handbook of Theoretical Computer Science, vol. B, chapter 6, pp. 243–320. MIT Press, 1990.

[DOS88] N. Dershowitz, M. Okada, G. Sivakumar. Confluence of conditional rewrite systems. In S. Kaplan, J.-P. Jouannaud, eds., Proc. 1st CTRS, LNCS 308, pp. 31–44. Springer, 1988.

[GS92] H. Ganzinger, J. Stuber. Inductive theorem proving by consistency for first-order clauses. In M. Rusinowitch, J.-L. Rémy, eds., Proc. of 3rd CTRS, LNCS 656, pp. 226–241. Springer, 1993.

[Kap87] S. Kaplan. Positive/negative conditional rewriting. In S. Kaplan, J.-P. Jouannaud, eds., Proc. 1st CTRS, LNCS 308, pp. 129–143. Springer, 1987.

[KM86] D. Kapur, D. R. Musser. Inductive reasoning with incomplete specifications. Prelim. report. In Proc. 1st LICS, Cambridge, MA, 1986.

[KM87] D. Kapur, D. R. Musser. Proof by consistency. Artificial Intelligence, 31:125–157, 1987.

[KR88] E. Kounalis, M. Rusinowitch. On word problems in Horn theories. In E. Lusk, R. Overbeek, eds., Proc. 9th CADE, LNCS 310 , pp. 527–535. Springer, 1988.

[KR90] E. Kounalis, M. Rusinowitch. Mechanizing inductive reasoning. In Proc. 8th AAAI, pp. 240–245. MIT Press, 1990.

[Pad90] P. Padawitz. Horn logic and rewriting for functional and logic program design. Technical Report MIP-9002, Univ. Passau, 1990.

[SNGM89] G. Smolka, W. Nutt, J.A. Goguen, J. Meseguer. Order-sorted equational computation. In H. Ait-Kaci, M. Nivat, eds., Proc. CREAS, vol. 2, Academic Press, 1989.

[Wal94] C. Walther. Mathematical induction. In Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, Clarendon Press, 1994.

[WG93] C.-P. Wirth, B. Gramlich. A constructor-based approach for positive/negativeconditional equational specifications. In M. Rusinowitch, J.-L. Rémy, eds., Proc. of 3rd CTRS, LNCS 656, pp. 198–212. Springer, 1993. Revised and extended version to appear in J. Symbolic Computation.

[WGKP93] C.-P. Wirth, B. Gramlich, U. Kühler, H. Prote. Constructor-based inductive validity in positive/negative-conditional equational specifications. SEKI-Report SR–93–05, FB Informatik, Univ. Kaiserslautern, 1993.

[Zha88] H. Zhang. Reduction, Superposition and Induction: Automated Reasoning in an Equational Logic. PhD thesis, Rensselaer Polytech. Inst., Troy, NY, 1988.

[ZKK88] H. Zhang, D. Kapur, M.S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In E. Lusk, R. Overbeek, eds., Proc. 9th CADE, LNCS 310, pp. 162–181. Springer, 1988.