Waldmeister
As you might already know, Waldmeister (asperula odorata, woodruff) is an ingredient for a very popular potable. It is also liked as aroma for sodas. But no, the Waldmeister we are talking about here, you cannot use for your potion. Well, maybe you try and make such a potion. If you are a logic-wizzard after drinking from it, please contact us... Because the Waldmeister we are talking about here is a highly efficient theorem prover for unit equational logic.
So be welcomed in the world of Waldmeister, which is the world of logical theorems.
Waldmeister is a theorem prover for unit equational logic. Its proof procedure is unfailing Knuth-Bendix completion [BDP89]. Waldmeister's main advantage is that efficiency has been reached in terms of time as well as of space. Within that scope, a complete proof object is constructed at run-time. Read more about the implementation.
All Time News
As in previous years, Waldmeister took part in the CASC prover competition, and came out first in its division.
For his book
Stephen Wolfram has employed our system to carry out investigations in the area of singleton axiom systems for Boolean algebra. Pages 809-10 therein show a proof found with Waldmeister that the equation
((x | y) | z) | (x | ((x | z) | x)) = z
axiomatizes the NAND Sheffer stroke. If you are more interested in the singleton subject, the Argonne group has already reported this result and more...