Efficient procedure for theorem proving in propositional logic on vector computers

[[abstract]]In this paper, we present an efficient procedure for solving the theorem proving problem in propositional logic. To take advantage of vector processing, we develop a vectorized representation of the problem and the deductions are performed implicity by simple AND and OR operations on vectors. The approach is simpler than those using explicit inference rules. Vectorized procedures based on the representation are then proposed. The computational bound of the approach on a concurrent-read exclusive-write parallel random access machine is of O(mlog2n), where m is the number of clauses and n is the number of distinct Boolean variables in the given formula. A divide-and-conquer strategy is used to partition the problem so that it can be solved by the existing vector computers. Experiments are conducted on vector computers. The result confirms the effectiveness of vectorization techniques and applicability of vector processing to theorem proving in propositional logic.[[fileno]]2030201010018[[department]]資訊工程學