Waldmeister Image

Waldmeister - A first try

This web interface gives you access to a resource-restricted version of Waldmeister running on our server.

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 defining the equational theory.


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

Choose either autonomous mode OR ordering and classification.

Autonomous Mode

Instead of specifying an ordering and a classification function, you can run Waldmeister in its autonomous mode.

Use autonomous mode.



Weights for KBO




Add-Weight Mix-Weight (default) Occnest


Copyright © 1998-2018 by Max-Planck-Institut für Informatik. All rights reserved.
Imprint / Impressum | Data Protection / Datenschutzhinweis

Document last changed on Wednesday, 16-May-2018