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: All these provers are in the Theorem Prover Museum.

Maria Paola Bonacina