SPASS Workbench
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.
SPASS Workbench