Implementation [of operators from axioms]

Given an axiom system in the form {f[a, f[a, a]]  a, 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^k2 - 1], With[{u = IntegerDigits[#, k, k²]}, 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⁴ 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.)