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.
|Titolo:||Distributed theorem proving by Peers|
|Data di pubblicazione:||1994|
|Appare nelle tipologie:||04.01 Contributo in atti di convegno|