Parallel Automated Reasoning and Clause-Graph Analysis

并行自动推理和子句图分析

• 批准号: 9003030
• 负责人: Steven Homer
• 金额: --
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1990
• 资助国家: 美国
• 起止时间: 1990-07-15 至 1991-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9003030&HistoricalAwards=false
• 关键词: Parallel; Automated; Reasoning; Clause; Graph

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.

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