We present an automated deduction system for equational reasoning combining two different parallelization/distribution schemes: Strategy-compliant parallelization on the level of individual deduction steps (PaReDuX) and distributed cooperation of multiple agents with different search strategies (Teamwork). In our experiments we mainly observed a multiplication of the speed-ups of each approach in our combined system.
Generated: 05/04/2002