| associativity | associativity4 | cac_redundancy | commutativity |
| associativity3 | c_associativity | cac_tautology | same_top |
int associativity(Term atom);If the atom is associativity, f(f(x,y),z) = f(x,f(y,z)), return the symnum of the operation; otherwise return 0 (which is never a symnum).
int associativity3(Term atom);If the atom is any of the following (ab)c = a(bc) (ab)c = a(cb) (ab)c = b(ac) (ab)c = b(ca) return the symnum of the operation; otherwise return 0 (which is never a symnum).
int associativity4(Term atom);If the atom is any of the following a(bc) = b(ac) a(bc) = b(ca) a(bc) = c(ab) a(bc) = c(ba) return the symnum of the operation; otherwise return 0 (which is never a symnum).
int c_associativity(Term atom);If the atom is c_associativity, f(x,f(y,z)) = f(y,f(x,z)), return the symnum of the operation; otherwise return 0 (which is never a symnum).
BOOL cac_redundancy(Topform c, BOOL print);This routine checks if the clause is commutativity or "c-associativity" x(yz)=y(xz); if so, it stores that information for later calls to cac_redundancy(). If an operation is found to C or AC, return TRUE; if found to be just A, return FALSE;
Otherwise, if any positive literal is an instance of x=x (mod C and AC as previously noted), it is rewritten to $T. Then return FALSE.
Motivation: If we know that * is commutative, and we derive an equation f(a,b*c)=f(a,c*b), we can delete that equation, because commutativity can do anything that equation can do. The same goes for AC operations.
BOOL cac_tautology(Literals lits);
int commutativity(Term atom);If the atom is commutativity, return the symnum of the operation; otherwise return 0 (which is never a symnum).
BOOL same_top(Term t1, Term t2);Do the two terms have the same top symbol?