Distributed theorem proving by Peers

Peers is a prototype for parallel theorem proving in a distributed environment. It implements a number of strategies for refutational, contraction-based theorem proving in equational theories, whose signatures may include associative-commutative (AC) function symbols. "Contraction-based" strategies is a more general term for "simplification-based", "rewriting-based" or "(Knuth-Bendix) completion-based" strategies. Such strategies are parallelized in Peers according to the Clause-Diffusion methodology for distributed deduction.