The DISCOUNT system (DIStributed COmpletion UsiNg
Teamwork) is a distributed theorem prover for pure unit-equality
problems that uses the unfailing Knuth-Bendix completion procedure as basic
calculus and the teamwork method as distribution
concept.
DISCOUNT features many different selection strategies for critical pairs that
are highly parameterized. The criteria used by the different strategies range
from statistical ones over goal-oriented ones to strategies that use learned
prior proof experience (see also our project
Learning
of search heuristics for theorem provers). By using teamwork, these
various strategies can cooperatively work together in finding a proof to a
given problem.
