Parallel Automated Reasoning and Clause-Graph Analysis

随着自动推理系统使用的增加和并行机的激增，对并行自动推理的研究的需求从未像现在这样明显。粗粒度并行定理证明器已经被开发出来，对于中小规模的问题表现出线性加速；然而，对于非常大的规模的问题，细粒度的证明器还没有开发出来。本文设计了一个基于子句图(或连接图)模型的SIMD并行自动推理系统。该系统将在CM-2型连接机上实现，并将应用于群论和组合几何中的一些问题。此外，还将开发并行算法来计算和分析子句图的谱。

With the increased use of automated reasoning systems and the proliferation of parallel machines, the need for research in parallel automated reasoning was never more evident. Coarse grain parallel theorem provers have been developed which demonstrate linear speed-up for small to medium scale problems; however, fine grain provers for very large scale problems have yet to be developed. In this work a SIMD parallel automated reasoning system will be designed based upon the clause graph (or connection graph) model. This system will be implemented on the Connection Machine model CM-2 and will be applied to a number of problems in group theory and combinatorial geometry. In addition, parallel algorithms will be developed for computing and analyzing the spectra of clause graphs.