Example is a set of axioms and conjectures of group theory. You can easily run the example or try out different axioms and conjectures.

To learn more about the use of Waldmeister, have a look on the Waldmeister primer, or see the references for further reading.

Input a set of equations to be proved. If none are input, Waldmeister tries to complete the equational theory.

f(sk,i(sk)) = f(i(sk),sk)

Choose either autonomous mode OR ordering and classification.

Use autonomous mode.

x,y,z,X,Y,Z

term1 = term2

+(a,b) = h(c,d)