Combining Parallel and Distributed Search in Automated Equational Deduction

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.

• Type: Conference
• Year: 2001
• Where: PPAM
• Authors: Carsten Sinz, Jörg Denzinger, Jürgen Avenhaus, Wolfgang Küchlin
• Keywords: Automated Deduction, Distributed And Parallel Computing, Different Parallelization/distribution Schemes, Individual Deduction Steps, PPAM 2001