.
After 795 inferences (24 seconds) a proof is achieved, and the following
extracted proof results.
% ui.gl, uniqueness of inverses in group
% domain elements
true => dom(e), dom(x), dom(y), dom(z).
% products
true => dom((y*x)), dom((x*y)), dom((x*z)).
% inverses
true => (x*z) = e, (y*x) = e, (x*y) = e .
% uniqueness of inverse
z = y => goal.
% equal is reflexite
X = Y => Y = X.
% equal is transitive
X = Y, Y = Z => X = Z.
% * is associative
dom(X), dom(Y), dom(Z) => ((X*Y)*Z) = (X*(Y*Z)).
% e is identity for *
dom(X) => (X*e) = X, (e*X) = X.
%% * preservation of equals
X = Y, dom(Z) => (Z*X) = (Z*Y), (X*Z) = (Y*Z).
Start GeologUI, and load ui.gl .
Repeatedly hit the inference button => on the toolbar. It is apparent that the associativity axiom (7th) can indefinitely produce new algebraic expressions which are equal, such as ...
(x*((x*z)*(x*y)))=((x*(x*z))*(x*y)) 409The complexity of inference fact 409 is 4 (4 operators max).
One would surmise that indefinitely complex terms are not needed to prove the uniqueness theorem (4th rule), but the last 3 rules can produce terms having unbounded complexity. Most likely, a minimum of 2 operators would be needed, so we set the complexity limit (* on current toolbar) to 2 and attempt a proof run. The rules that introduce more complex terms are still applied but not if the complexity (number of operators) is greater than 2. This works! (If it had not we would have tried 3, etc.)
To reproduce this result,
set the run limit to 1000 and then run
.
After 795 inferences (24 seconds) a proof is achieved, and the following
extracted proof results.
