Thomas Hillenbrand (MPI, Saarbrücken) FAST EQUATIONAL REASONING WITH WALDMEISTER ---------------------------------------------------------------------- For automated reasoning in structures that are axiomatized by equations, Knuth-Bendix completion and its refinements are the method of choice today. The Waldmeister system is among the strongest implementations thereof, as demonstrated repeatedly in last years' competitions at the Conference on Automated Deduction. In the talk, the concepts underlying this theorem prover will be surveyed. Using a variant of the given-clause algorithm, the prover saturates the input axiomatization in a repeated cycle that works on a set of active and a set of passive facts, where the latter are the one-step inference conclusions of the former up to redundancy. This system architecture is realized via specifically tailored representations for each of the central data structures: indexing for the active facts, group-wise compression for the passive facts, successor sets for the conjectures. Empirically gained control knowledge has been integrated, such that the system often is easier to use. In order to cope with large search spaces, specialized redundancy criteria are employed, for example based on ground joinability or ground reducibility and exploiting the technology of ordering constraints. To mention a fruitful application, S. Wolfram employed the prover in writing "A New Kind of Science" for deriving minimal axiomatizations of the Sheffer stroke. These successful experiments initiated the integration of Waldmeister into the Mathematica computer algebra system.