Distributed automated deduction
Maria Paola Bonacina · 1992
This thesis comprises four main contributions: an abstract framework for theorem proving, a methodology for parallel theorem proving in a distributed environment, termed deduction by Clause-Diffusion, a study of special topics in distributed deduction with contraction and an implementation, the theorem prover Aquarius, of the Clause-Diffusion methodology. In our abstract framework, a theorem proving derivation is conceived as a process of reducing a proof of the target or goal. The most important feature of our framework is that it provides the first notion of fairness for theorem proving, which is weaker than the fairness property required to generate confluent systems. A weaker fairness requirement is a theoretical pre-condition to the design of more efficient theorem proving strategies. The Clause-Diffusion methodology exploits parallelism at the search level, by having concurrent, asynchronous deductive processes searching in parallel the search space of the problem. This methodology has been designed to provide solutions to the problems in the parallelization of contraction-based strategies. We describe backward contraction, the task of maintaining clauses reduced in a dynamically changing data base, as the main obstacle in parallel theorem proving with contraction. If a finer granularity of parallelism is adopted, e.g. parallelism at the clause level in shared memory, this difficulty appears as a write-bottleneck, which we have called the backward contraction bottleneck. The Clause-Diffusion approach avoids this problem by adopting a mostly distributed memory and distributed global contraction schemes. We have given a definition of distributed derivations and characterized their fairness requirements. We have observed that the uncontrolled application of subsumption in a distributed data base may violate the fairness and the monotonicity of distributed derivations. This discovery has propelled a re-examination of the subsumption inference rule, which we view as a replacement rule, rather than a deletion rule. Our new distributed subsumption inference rule preserves both fairness and monotonicity, without reducing the contraction power of subsumption. We conclude with the description of the distributed theorem prover Aquarius, including some experiments, and with directions for future research, such as the design of parallel search plans. (Abstract shortened by UMI.)