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.

Conjectures

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.

Autonomous Mode

Use autonomous mode.

Ordering

Classification

Conventions

• Variables start with x,y,z,X,Y,Z.
• Equations have the form term1 = term2. Each line should contain exactly one equation.
• Prefix notation has to be used, e.g. +(a,b) = h(c,d).
• The equations are considered as implicitly universally quantified over their variables, whereas existantial quantifications have to be expressed via skolemization.
• The set of hypotheses (goals) are implicitly existentially quantified, and universal quantification must be expressed via skolemization. Existential quantification is allowed for at most one hypothesis.