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.


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-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.