How to use Waldmeister | Example for a correct input file | Output from a successful proof | General Overview | Command Line Options | Additional Remarks
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.
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) |
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.)
(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
|
Section SIGNATURE contains
the declaration of identifiers for operators, i.e. functions and constants. |
||
| 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. |
||
| 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
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.
********************************************************************************
****************************** COMPLETION - PROOF ********************
********************************************************************************
|
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.
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.
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. |
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.