Distributed theorem proving and the Clause-Diffusion method

Logic-based computation is characterized by the distinction between the logic (in theorem-proving strategies, the inference system) and the control (the search plan). Since the logic itself does not assume that the computation is sequential, logic-based computation has been regarded as suitable for parallelization. This notion emerged first in logic programming and in rewriting-based equational programming, and migrated later to automated theorem proving, SAT-solving, and constraint reasoning in general: I proposed the Clause-Diffusion method for distributed deduction, where concurrent, asynchronous, deductive processes search in parallel for a proof, realizing the principle of parallelism at the search level: Clause-Diffusion evolved into Modified Clause-Diffusion: I worked on the implementation of several Clause-Diffusion theorem provers, and Clause-Diffusion inspired the first divide-and-conquer approach to parallel SAT-solving:


Maria Paola Bonacina