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
Note: 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 | 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 | 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. | ||
SIGNATURE
| Section SIGNATURE contains the declaration of identifiers for operators, i.e. functions and constants. | ||
ORDERING | 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. | ||
VARIABLES | In section VARIABLES, identifiers for variables are declared along with their sorts. | ||
EQUATIONS | Section EQUATIONS contains the axioms defining the equational theory. | ||
CONCLUSION | 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 |
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:
- Waldmeister proves all hypotheses and terminates (proof mode only).
- Waldmeister derives a finite ground convergent set of rewrite rules, which is used to normalize the hypotheses. Validity is now equivalent to joinability. Especially, this is the only possibility to show that an equation s=t does not hold in all models of E!
Otherwise, one afterwards does not know anything more than before:
- The prover fails due to insufficient memory.
- The prover does not produce anything useful within reasonable time.
- With flag "--auto" set and fairness lost, Waldmeister runs out of critical pairs.
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
Waldmeister shows, which rules where created. Here only the rules that where used are mentioned.
| 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 |
This proves the goal
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.
Proved Goals:
No. 1: f(e,sk) ?= sk joined, current: sk = sk
1 goal was specified, which was proved.
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.
Statistics:
-----------
Rules 9
Equations 0
Critical pairs 34
Process size 1876000
Search time [s] 0.2
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.
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.