WALDMEISTER: Development of a High Performance Completion-Based
Theorem Prover

Arnim Buch, Thomas Hillenbrand
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, 67653 Kaiserslautern
Germany
E-mail: buch@informatik.uni-kl.de
        hillen@informatik.uni-kl.de

Abstract
In this report we give an overview of the development of our new
WALDMEISTER prover for equational theories. We elaborate a
systematic stepwise design process, starting with the inference
system for unfailing Knuth-Bendix completion and ending up with
an implementation which avoids the main diseases today's provers
suffer from: overindulgence in time and space.

Our design process is based on a logical three-level system
model consisting of basic operations for inference step
execution, aggregated inference machine, and overall control
strategy. Careful analysis of the inference system for unfailing
completion has revealed the crucial points responsible for time
and space consumption. For the low level of our model, we
introduce specialized data structures and algorithms speeding up
the running system and cutting it down in size - both by one
order of magnitude compared with standard techniques.  Flexible
control of the mid-level aggregation inside the resulting prover
is made possible by a corresponding set of parameters.
Experimental analysis shows that this flexibility is a point of
high importance. We go on with some implementation guidelines we
have found valuable in the field of deduction.

The resulting new prover shows that our design approach is
promising.  We compare our system's throughput with that of an
established system and finally demonstrate how two very hard
problems could be solved by WALDMEISTER.


Keywords
automated deduction, equational logic,
high performance completion procedure, term indexing

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1996/
file: Buch.SR-96-01.ps.gz