B. Pradeep et Csr. Murthy, A CONSTANT-TIME ALGORITHM FOR THEOREM-PROVING IN PROPOSITIONAL LOGIC ON RECONFIGURABLE MESHES, Information sciences, 85(1-3), 1995, pp. 175-184
Citations number
16
Categorie Soggetti
Information Science & Library Science","Computer Science Information Systems
In this paper, we present an O(1) time algorithm for theorem proving i
n propositional logic on processor arrays with a reconfigurable bus sy
stem of size m x 2(n), where m is the number of clauses and n is the n
umber of Boolean variables. The theorem proving problem involves combi
natorial exploration of an exponential search space. Our approach to t
he problem is simpler than using explicit inference rules, as the prob
lem is vectorized and deductions are performed implicitly by simple AN
D and OR operations on vectors. The previous best parallel algorithm f
or the theorem proving problem available in the literature has a time
complexity of O(mlog(2)n) using O(2(n)) processors. Thus, our algorith
m is faster and further; costwise (time complexity x number of process
ors), it is efficient by a factor of log(2)n.