Implementation [of operators from axioms]

Given an axiom system in the form {LongEqual[f[a,f[a,a]],a], LongEqual[f[a,b],f[b,a]]} one can find rule numbers for the operators f[x, y] with k values for each variable that are consistent with the axiom system by using

Module[{c, v}, c = Apply[Function, {v = Union[Level[axioms, {-1}]], Apply[And, axioms]}]; Select[Range[0, k^(k^{2}) - 1], With[{u = IntegerDigits[#, k, k^{2}]}, Block[{f}, f[x_, y_] := u[[-1 - k x - y]]; Array[c, Table[k, {Length[v]}], 0, And]]] &]]

For k=4 this involves checking nearly 16^{4} or 4 billion cases, though many of these can often be avoided, for example by using analogs of the so-called Davis–Putnam rules. (In searching for an axiom system for a given operator it is in practice often convenient first to test whether each candidate axiom holds for the operator one wants.)