Joerg Denzinger, Martin Kronburg, Stephan Schulz: "DISCOUNT - A
distributed and learning equational prover"

Abstract:

The DISCOUNT system is a distributed equational theorem prover based
on the teamwork method for knowledge-based distribution. It uses an
extended version of unfailing Knuth-Bendix completion that is able to
deal with arbitrarily quantified goals. DISCOUNT features many
different control strategies that cooperate using the teamwork
approach. Competition between multiple strategies, combined with
reactive planning, results in an adaptation of the whole system to
given problems, and thus in a very high degree of independence from
user interaction.

Teamwork also provides a suitable framework for the use of control
strategies based on learning from previous proof experiences. One of
these strategies forms the core of the expert global_learn, which is
capable of learning from successful proofs of several problems. This
expert, running sequentially, was one of the entrants in the
competition (DISCOUNT/GL), while a distributed DISCOUNT system running
on two workstations was another entrant.