Parallelism

The late nineteen-eighties saw the impact of parallel computing on almost all aspects of computer science. Automated theorem proving offers the potential for doing a great deal of its computations in parallel, although the maintenance of a coherent state of knowledge dictated by the closure approach makes the problem non-trivial, and the problem of redundancy control is accentuated. Indeed, parallelism in symbolic fields such as theorem proving can be considerably more challenging than in many traditional numerical areas, where regular patterns of uniform parallelism are common. Two quite different approaches to parallelizing the closure approach have been tried so far, one for each of the two major computational models for MIMD computation. In each case, a modification of the closure algorithm is needed, but not a fundamental change.