In this paper, it is shown that there is an algorithm that, given by finite set E of ground equations, produces a reduced canonical rewriting system R equivalent to E in polynomial time. This algorithm based on congruence closure performs simplification steps guided by a total simplification ordering on ground terms, and it runs in time O(n 3 ) .

In this paper, it is shown that the method of matings due to Andrews and Bibel can be extended to (first-order) languages with equality. A decidable version of E -unification called rigid E-unification is introduced, and it is shown that the method of equational matings remains complete when used in conjunction with rigid E -unification. Checking that a family of mated sets is an equational mating is equivalent to the following restricted kind of E -unification. Problem Given E → ={E i | 1≤i≤n} a family of n finite sets of equations and S={〈u i ,v i 〉 |1≤i≤n} a set of n pairs of terms, is there a substitution θ such that, treating each set θ(E i ) as a set of ground equations (i.e., holding the variables in θ(E i ) “rigid”), θ(u i ), and θ(v i ) are provably equal from θ(E i ) for i=1,...,n? Equivalently, is there a substitution θ such that θ(u i ) and θ(v i ) can be shown congruent from θ(E i ) by the congruence closure method for i=1,...,n? A substitution θ solving the above problem is called a rigid E → -unifier of S , and a pair 〈E → ,S〉 such that S has some rigid E → -unifier is called an equational premating. It is shown that deciding whether a pair 〈 E → ,S〉is an equational premating is an NP-complete problem.

We study the effect of adding a rule to a rule‐based heuristic classification expert system, in particular, a rule that causes an unforeseen interaction with rules already in the rule set. We show that it is possible for such an interaction to occur between sets of rules, even when no interaction is present between any pair of rules contained in these sets. A method is presented that identifies interactions between sets of rules, and an analysis is given which relates these interactions to rule‐based programming practices which help to maintain die integrity of the knowledge base. We argue mat the method is practical, given some reasonable assumptions on the knowledge base.