How to use Waldmeister | Example for a correct input file | Output from a successful proof | General Overview | Command Line Options | Additional Remarks


How to use Waldmeister

The following mainly refers to the Waldmeister distribution which you can download. You can also just try out Waldmeister with a web form we provide.

The language of Waldmeister consists of equations that are considered as implicitly universally quantified over their variables, whereas existential quantifications have to be expressed via skolemization.
Details you could find in an introduction to logics for computer scientists.

Waldmeister is an automatic prover. To show its use, we start with a relatively simple example.

Lets say we want to prove that for every x in a group, x+(-x) = (-x)+x. We already know that in a group, there exists an element e such that for all members x of the field, x+e=x. Likewise we know that for every element x there exists an -x, so that x+(-x)=e

For a short explication on how Waldmeister works see the implementation section or the references with further reading.

Example:

The defining properties of a group are :

Property

f means addition, i fixes/finds the inverse of an element in a field

There exists an e such that for all x, x+e = x f(x,e) = x
For all x exists an (-x), such that x+(-x) = e f(x,i(x)) = e
For all x and z in a field is (x+y)+z = x+(y+z) f(f(x,y),z) = f(x,f(y,z))

 

Say you want to prove that

for every x in a group is
x+(-x) = (-x)+x
f(sk,i(sk)) = f(i(sk),sk)

 

 

Syntax

Now that we have translated the problem and the properties of a group in an appropriate language which Waldmeister will understand, we still need to "feed" Waldmeister with the equations we got. In addition, Waldmeister needs a few more informations about what we want him to do and how. To give these, we put together an input file with the following elements.

(The input file is necessary for the distribution, which you can download. For a first try, just use the www form.)

Example of a correct input file

(This example you also find included in the distribution. Remark: explications have been slightly simplified for better understanding. For a more in-depth look see some of the articles on the references page.)

A correct Input file for Waldmeister could look like this. You can call Waldmeister giving it the name of the inputfile as an input parameter.

NAME group % what else

In section NAME, a name for the subsequent specification is given. Note that the character "%" declares the rest of the line to be a comment.

MODE PROOF
% COMPLETION
The section MODE contains one of the keywords PROOF and COMPLETION to determine what to do with the specification. PROOF denotes the ordinary proof mode, whereas in completion mode Waldmeister tries to derive a finite convergent set of rules from the specification and - if successful - decides if the conjectives hold.
SORTS ANY
% ANY1 ANY2
In section SORTS, the identifiers of the sorts the operators shall work on and the variables may belong to are declared. In the following, none but these sort identifiers may be used.
The signature Waldmeister accepts is many-sorted. There are no sort hierarchies, and all sorts are considered disjoint.
SIGNATURE
e:
i: ANY
f: ANY ANY
sk:

-> ANY
-> ANY
-> ANY
-> ANY

Section SIGNATURE contains the declaration of identifiers for operators, i.e. functions and constants.
Also, the argument sorts and the single target sort are stated.
In this example, i:ANY->ANY means: the function
symbol i takes an operand of sort ANY and yields an element of the same sort.

ORDERING
LPO
i > f > e > sk
% alternatively:
% KBO
% i=0, f=1, e=1, sk=1
% i > f > e > sk

In section ORDERING, a reduction ordering to orient rules with is specified: either a lexicographic path ordering ("LPO"), based on an operator precedence, or an extended Knuth-Bendix ordering ("KBO" with a weight for each operator and an additional operator precedence for the comparison of equally weighted terms.
For mode PROOF, the precedence has to be total.

VARIABLES
x,y,z : ANY
In section VARIABLES, identifiers for variables are declared along with their sorts.
EQUATIONS
f(x,e) = x
f(x,i(x))=e
f(f(x,y),z)=f(x,f(y,z))

Section EQUATIONS contains the axioms defining the equational theory.

CONCLUSION
f(sk,i(sk)) = f(i(sk),sk)
Section CONCLUSION holds a set of hypotheses to be proved, which may be empty only in completion mode. In proof mode, Waldmeister terminates as soon as all hypotheses are
shown.
Note: Vice versa to section EQUATIONS, variables are implicitly existentially quantified, and universal quantification must be expressed via skolemization. Existential quantification is allowed in proof mode only, and for not more than one hypothesis.

To try out the above example just install Waldmeister and find this example in the distribution. Just move to the Waldmeister directory and type
bin/waldmeister example.pr

 

Output from a successful proof

A system header appears, and Waldmeister prints out a protocol of the proof process on the level of selected facts (rules).

There are five different types of behaviour. The pleasing ones are the following:

Otherwise, one afterwards does not know anything more than before:

More precisely, in all three cases no conclusions concerning validity of yet unproved conjectives may be drawn! Similarly, a finite ground convergent set of rewrite rules that is oriented with the specified ordering and is equivalent to the initial equations might exist nevertheless!

If the prover fails, re-adjustment of the control parameters may be helpful. Changing the top-level heuristic is a matter of command line modifications. Apart from that, we have to stress the importance of the adequate choice of reduction ordering: A proof that is impossible to find
within hours may be found within milliseconds when changing from KBO to LPO or vice versa, or changing the operator precedence in case of LPO!

The question of how to make this choice skillfully is difficult to answer. Roughly speaking, the Knuth-Bendix ordering leads to shorter simplification chains, and should be preferred in general. In the presence of a distributivity law, however, it is often useful to apply that law for splitting product terms, which requires the use of a lexicographic path ordering with a precendence where the multiplication symbol is greater than the addition symbol.
Generalizing this proceeding, you should always make a selection which orients the initial equations in a way that seems natural to you. Finally, Skolem constants should always be minimal in the precedence.

You might want to read a more in depth description of Waldmeister's abilities.

Output from the Input file above

After a few preliminaries, as the repetition of the input (see above), Waldmeisters output by our example proof looks as follows:

********************************************************************************
****************************** COMPLETION - PROOF ********************
********************************************************************************

new rule: 1 f(f(x1,x2),x3)-> f(x1,f(x2,x3))
new rule: 2 f(x1,e) -> x1
new rule: 3 f(x1,i(x1)) -> e
new rule: 4 f(x1,f(e,x2)) -> f(x1,x2)
new rule: 5 f(x1,i(e)) -> x1
new rule: 6 f(x1,f(i(x1),x2)) -> f(e,x2)
new rule: 7 f(e,i(i(x1))) -> x1
new rule: 8 f(x1,i(i(x2))) -> f(x1,x2)
remove rule: 7  
new rule: 9 f(e,x1) -> x1
remove rule: 4  
simplify rhs of rule: 6  
joined goal: 1 f(e,sk) ?= sk to sk

Waldmeister shows, which rules where created

Here only the rules that where used are mentioned.

 

+--------------------------+
| this proves the goal |
+--------------------------+

Proved Goals:
No. 1: f(e,sk) ?= sk joined, current: sk = sk
1 goal was specified, which was proved.
Waldmeister states, that the goal number on, f(e,sk)=sk, is proved. The question marks states that this is what has to be proved.

 

Statistics:
-----------
Rules 9
Equations 0
Critical pairs 34
Process size 1876000
Search time [s] 0.2

Waldmeister also tells you some statistical facts: how many rules, how many equations, how many critical pairs had to be created until the proof whas found.

 

 

Finally there is a third program, created by Stephan Schulz, used to produce a human readable proof.


General Overview

In outline, the task Waldmeister deals with is the following: A theory is formulated as a set E of implicitly universally quantified equations over a many-sorted signature. It shall be demonstrated that a given equation s=t is valid in this equational theory, i.e. that it holds in all models of E. Equivalently, s is deducible from t by applications of the axioms of E, substituting equals for equals.

In 1970, Knuth and Bendix presented a completion algorithm, which later was extended to unfailing completion, as described e.g. by Bachmair et al. Parameterized with a reduction ordering, the unfailing variant transforms E into a ground convergent set of rewrite rules.

Accordingly, when searching for a proof, Waldmeister saturates the given axiomatization until the conjectures can be shown by narrowing or rewriting. The saturation is performed in a cycle working on a set of active (selected) facts and a set of passive (waiting) facts (rules). Inside the completion loop, the following steps are performed:

1. Select an equation from the set of passive facts.
2. Simplify this equation to a normal form.
3. Modify the set of rules according to the equation.
4. Generate all new critical pairs.
5. Add the equation to the set of rules.

The selection is controlled by a top-level heuristic maintaining a priority queue on the critical pairs. This top-level heuristic is one of the two most important control parameters. The other one is the reduction ordering to orient rules with. There is some evidence that the latter is of even stronger influence.

 

Command Line Options (for the distribution)


According to GNU standards, the command line options start with a double hyphen, followed by the option name, such as "--sunshine" or "--lunch=hot-pot".

--help The most helpful option of all is "--help", which makes Waldmeister display a short overview of the command line options available and terminate.
--man With the option "--man" a more detailed, "man page"-like documentation is displayed.
--version With option "--version" set, Waldmeister prints out its version information and terminates as well.

The remaining options are divided into such controlling the proof search, As to the first, there are two different functions for weighting critical pairs, realizing well-behaved general purpose top- level heuristics.

 

There are four different output formats, not more than one of which may be selected via a command line option:

--ascii processed proof as plain text (default)
--tex the same as LaTeX source file
--prolog the same in a PROLOG-like notation
--pcl step-wise internal proof object
--details For ASCII and LaTeX output format, setting the option enriches the proof with more detailed information, such as variable instantiations in lemma applications.
--output=<Filename> Redirects the output to the named file.

Additional Remarks

The executable named "proof" should be located in the same directory as the Waldmeister executable. If Waldmeister fails in calling it, this directory should be added to the path variable of the shell.

Stephan Schulz has written a tool named "lemma" with many possibilities to control the processing of the proof. This tool is included in the Waldmeister distribution as well. It takes the step-wise internal proof object as input. Call "lemma -h" for an online documentation (German language only).

Together with the Waldmeister distribution comes a set of problems yopu could use to test Waldmeister's abilities. Namely the unit equality problems of the TPTP (Thousands of Problems for Theorem Provers) Problem Library, version 2.4.1, in Waldmeister format is included in the Waldmeister distribution. Of course, the complete library also has tools for automatic conversion to Waldmeister format, but this increases your ease of use, especially if you have not installed a Prolog interpreter. - For an overview, you also get the current TPTP ReadMe file.


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 Friday, 08-Aug-2003 13:36:34 MEST.