The Clause-Diffusion theorem provers

Clause-Diffusion is a general methodology for distributed deduction by distributed search: the search space of the theorem proving problem is subdivided among concurrent asynchronous deductive processes, each generating a derivation and keeping a database of clauses. A distributed derivation is given by the collection of these derivations, and it succeeds as soon as one of them does. A Clause-Diffusion strategy is defined by an inference system and a parallel search plan, executed by each process. The parallel search plan controls the selection of inferences, like in sequential search, their subdivision, with a choice of subdivision criteria, and the diffusion of clauses by broadcasting. There is no need for a master or top-level scheduler to distribute the work: the subdivision of inferences is achieved dynamically by the processes, by subdividing the clauses, hence the inferences. The following Clause-Diffusion provers were developed:

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 3rd 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 (Project summary). In Proceedings of the 1st 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 Jieh Hsiang. The Clause-Diffusion methodology for distributed deduction. Fundamenta Informaticae, 24(1,2):177-207, September 1995; DOI: 10.3233/FI-1995-24128.
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 1996 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 14th 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 2nd International Symposium on Parallel Symbolic Computation (PASCO), Wailea, Maui, Hawaii, July 1997. ACM Press, 88-100, 1997; DOI: 10.1145/266670.266696 (©[ACM Inc.][1997]).
  In May 1998, Peers-mcd.b succeded in solving the 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 15th International Conference on Automated Deduction (CADE), July 1998.
- 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.
  For each mode, the prover implements various strategies described in
  - 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.
  together with experiments showing that Peers-mcd.d can prove the Moufang identities in alternative rings without cancellation laws and exhibiting instances of super-linear speed-up due to parallel search.

All these provers are in the Theorem Prover Museum.

Maria Paola Bonacina