Parallel execution of mechanical theorem proving procedures

[[abstract]]©1994 Scientific World-Parallel processing is a key methodology for speeding up problem solving, especially for many computation-intensive problems that often arise in scientific, engineering and AI application areas. We consider parallel processing of the theorem proving problem that involves intensively combinatorial exploration of a solution space. Mechanical theorem proving is known to be NP-complete in propositional logic and undecidable in first-order logic. It is thus desirable to consider parallel approaches to tackle such hard problems. We begin with reviews of several results regarding special instances of the theorem proving problem which are known to be polynomially solvable. Most problems can be reduced to specific problems in directed graphs, and we thus take advantage of parallel graph algorithms to solve them. Then, parallel approaches for propositional formulas are described, each of which either parallelizes or vectorizes the rules involved in the Davis-Putnam (1960) procedure, and thus is shown to have great relevance to the procedure. Finally, we give parallel algorithms for first-order formulas. One approach generates propositional formulas from the given first-order formulas and makes use of parallel algorithms for propositional formulas to deal with them, while the other avoids the generation of propositional formulas by means of a parallel inference rule to perform the deduction directly. We show that, by using these approaches, a considerable amount of parallelism can be rendered in the solving of the theorem-proving problem and can therefore accelerate the execution of proof procedures.[[department]]資訊工程學