**Aquarius (January 1992 - December 1992)**was developed for workstation networks (each deductive process runs on a workstation) at SUNY Stony Brook in the spring and summer of 1992, as part of my Phd thesis, and experimentation continued till the end of that year. Aquarius was the Clause-Diffusion parallelization of Otter (version 2.2). The logic is first-order logic with equality, and the code is written in C, using the high-level language PCN for parallelism and communication:- Maria Paola Bonacina and Jieh Hsiang. Distributed deduction by Clause-Diffusion: distributed contraction and the Aquarius prover. Journal of Symbolic Computation, 19:245-267, January-March 1995; DOI: 10.1006/jsco.1995.1014.
- Maria Paola Bonacina and Jieh Hsiang.
Distributed
deduction by Clause-Diffusion: the Aquarius prover.
In
*Proceedings of the Third International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO)*, Gmunden, Austria, September 1993. Springer, Lecture Notes in Computer Science 722, 272-287, 1993; DOI: 10.1007/BFb0013183. - Maria Paola Bonacina and Jieh Hsiang.
A system for distributed simplification-based theorem proving.
In
*Proceedings of the First International Workshop on Parallelization in Inference Systems*, Schloss Dagstuhl, Germany, December 1990. Springer, Lecture Notes in Artificial Intelligence 590, 370-370, 1992; DOI: 10.1007/3-540-55425-4_18.

**Peers (January 1993 - May 1995)**was developed for workstation networks at the Argonne National Laboratory in January-February 1993. Peers is a Clause-Diffusion prover for equational theories, possibly modulo associativity and commutativity. It was written in C using p4 for message-passing, and incorporating code from the*Otter Parts Store*(version of December 1992). Its name emphasizes that all processes in Clause-Diffusion are peers, with no master-slave relation. Peers and its experiments up to March 1994 were presented in:- Maria Paola Bonacina and
William W. McCune.
Distributed theorem
proving by Peers.
*Proceedings of CADE-12*, Springer, Lecture Notes in Artificial Intelligence 814, 841-845, 1994; DOI: 10.1007/3-540-58156-1_72.

- Maria Paola Bonacina and
William W. McCune.
Distributed theorem
proving by Peers.
**Peers-mcd**was the successor of Peers, implementing Modified Clause-Diffusion rather than Clause-Diffusion. Four versions were developed:**Peers-mcd.a (June 1995 - September 1996)**was written in June 1995. The experimentation up to October 1995 is reported in:- Maria Paola Bonacina. On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method. Journal of Symbolic Computation, 21(4-6):507-522, April-June 1996; DOI: 10.1006/jsco.1996.0028.

**Peers-mcd.b (October 1996 - January 1999):**work on Peers-mcd restarted in June 1996, and in October 1996 a completely new Peers-mcd theorem prover (Peers-mcd.b) was built on top of the Argonne prover EQP (version 0.9), that had just proved that Robbins algebras are Boolean. Peers-mcd was written in C using MPI for message-passing, and was ported on both workstation networks and multiprocessors. In addition to a different implementation, Peers-mcd differed from its predecessors because it featured a new family of criteria for subdivision of clauses, the*Ancestor-Graph Oriented criteria*, or*AGO criteria*for short. The theorem prover, the AGO criteria, and the experimental results up to the summer of 1997, including*instances of super-linear speed-up*on two lemmas that represent two thirds of the proof of the Robbins problem, are described in:- Maria Paola Bonacina.
The Clause-Diffusion
theorem prover Peers-mcd.
In
*Proceedings of the Fourteenth International Conference on Automated Deduction (CADE)*, Springer, Lecture Notes in Artificial Intelligence 1249, 53-56, 1997; DOI: 10.1007/3-540-63104-6_6. - Maria Paola Bonacina.
Experiments with subdivision of search in distributed theorem proving.
In
*Proceedings of the Second International Symposium on Parallel Symbolic Computation (PASCO)*(©Copyright 1997 by ACM, Inc.) Wailea, Maui, Hawaii, July 1997. ACM Press, 88-100, 1997; DOI: 10.1145/266670.266696.

*Levi Commutator Problem*in Group Theory, that had been given as a challenge at the CADE-15 Workshop on Problem Solving Methodologies with Automated Deduction:- Maria Paola Bonacina.
Mechanical
proofs of the Levi commutator problem.
Workshop on Problem Solving Methodologies with Automated Deduction,
at the
*Fifteenth International Conference on Automated Deduction (CADE)*, July 1998.

- Maria Paola Bonacina.
The Clause-Diffusion
theorem prover Peers-mcd.
In
**Peers-mcd.c (February 1999 - March 2000)**was written in the spring of 1999 with version 0.9d of EQP as sequential base. The Robbins experiments were repeated, confirming the super-linear speed-up in the first two lemmas that form the proof of the Robbins conjecture, and obtaining an almost linear speed-up in the third. These experiments are described in:- Maria Paola Bonacina. A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence, 29(1-4):223-257, 2000; DOI: 10.1023/A:1018932114059.

**Peers-mcd.d (April 2000 - July 2001)**was developed in the spring and summer of 2000, making available in the framework of Modified Clause-Diffusion both distributed search and*multi-search*, that differentiates the searches generated by the parallel processes by assigning them different search plans. Peers-mcd.d can work in three modes:*Pure distributed-search mode:*search space subdivided among the processes - all processes execute the same search plan.*Pure multi-search mode:*search space not subdivided - every process executes a different search plan.*Hybrid mode:*search space subdivided - the processes execute different search plans.

- Maria Paola Bonacina.
Combination of distributed search and multi-search in Peers-mcd.d.
In
*Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR)*, Siena, Italy, June 2001. Springer, Lecture Notes in Artificial Intelligence 2083, 448-452, 2001; DOI: 10.1007/3-540-45744-5_37.

*Moufang identities in alternative rings*without cancellation laws and exhibiting instances of super-linear speed-up due to parallel search.