hide
Free keywords:
-
Abstract:
In the last years, the development of automated theorem
provers has been advancing in a so to speak Olympic spirit,
following the motto "faster, higher, stronger"; and the
{Waldmeister} system has been a part of that endeavour. We
will survey the concepts underlying this prover, which
implements Knuth-Bendix completion in its unfailing variant.
The system architecture is based on a strict separation of
active and passive facts, and is realized via specifically
tailored representations for each of the central data
structures: indexing for the active facts, set-based
compression for the passive facts, successor sets for the
conjectures. In order to cope with large search spaces,
specialized redundancy criteria are employed, and the
empirically gained control knowledge is integrated to ease
the use of the system. We conclude with a discussion of
strengths and weaknesses, and a view of future prospects.
