A parallel approach for theorem proving in propositional logic (Q1102766)

The divide-and-conquer strategy and a pipelining discipline are applied to theorem proving in propositional logic. The strategy is itself logically complete and sound. Based on this strategy a parallel proof procedure can be constructed. With a pipelined execution model, we show that the processing time using our parallel approach to solve such an NP- complete problem is of O(mn), where m is the number of clauses and n is the number of distinct Boolean variables in the given formula. The approach is simpler than those using explicit inference rules, since the deductions are performed implicitly by only simple checking and deleting operations on each clause.