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.

Axioms

Input a set of equations defining the equational theory.

Conjectures

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.


Ordering

KBO

Weights for KBO

LPO

Precedences

Classification

Add-Weight Mix-Weight (default) Occnest

Conventions



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