Waldmeister - A first try


This WWW 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-2007 by Max-Planck-Institut für Informatik. All rights reserved.
Imprint and legal notices. www site design and concept by Doris Diedrich.

Document last changed on Wednesday, 17-Oct-2007 11:05:54 MEST.