This Article 
 Bibliographic References 
 Add to: 
Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers
October 1992 (vol. 4 no. 5)
pp. 475-486

Vectorization techniques for solving the theorem-proving problem in propositional logic on vector computers is presented. To take advantage of vector processing, the rules used in the deduction process are first generalized by considering more than one literal at a time. The soundness of the generalized rules is proved. The vectorized representation of the problem and algorithms based on the generalized rules is proposed. Experiments conducted on vector computers show that the vectorized procedure is effective.

[1] C. L. Chang and R. C. T. Lee,Symbolic Logic and Mechanical Theorem Proving. New York: Academic, 1973.
[2] W. T. Chen and M. Y. Fang, "Vectorization techniques for theorem proving in propositional logic," inProc. 1990 Int. Conf. on Parallel Processing, St. Charles, IL, Aug. 1990, pp. II-229-II-235.
[3] W. T. Chen and L. L. Liu, "Parallel approach for theorem proving in propositional logic,"Inform. Sci., vol. 41, no. 1, pp. 61-76, 1987.
[4] S. A. Cook, "The complexity of theorem-proving procedures," inProc. 3rd Annu. ACM Symp. Theory of Comput., 1971, pp. 151-158.
[5] M. Davis and H. Putnam, "A computing procedure for quantification theory,"J. Ass. Comput. Mach., vol. 7, no. 3, pp. 201-215, 1960.
[6] M. R. Garey and D. S. Johnson,Computers and Intractability: A Guide to Theory of NP-Completeness. San Francisco, CA: Freeman, 1979.
[7] K. Hwang and F. A. Briggs,Computer Architecture and Parallel Processing. New York: McGraw-Hill, 1984.
[8] K. Hwang, "Multiprocessor supercomputers for scientific engineering application,"Comput., vol. 18, no. 6, pp. 57-73, June 1985.
[9] D. W. Loveland,Automated Theorem Proving: A Logic Basis. Amsterdam, The Netherlands: North-Holland, 1978.
[10] D. W. Loveland, "Automated theorem proving: A quarter century review,"Contemporary Math., vol. 29, pp. 1-45, 1984.
[11] Scientific Supercomputer Subcommittee, "Software for supercomputers,"Computer, vol. 21, no. 12, pp. 70-74, Dec. 1988.
[12] A. Urquhart, "Hard examples for resolution,"J. Ass. Comput. Mach., vol. 31, no. 1, pp. 209-219, 1987.

Index Terms:
vectorisation; deduction rules; theorem proving; propositional logic; vector computers; artificial intelligence; formal logic; theorem proving; vector processor systems
M.-Y. Fang, W.-T. Chen, "Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers," IEEE Transactions on Knowledge and Data Engineering, vol. 4, no. 5, pp. 475-486, Oct. 1992, doi:10.1109/69.166989
Usage of this product signifies your acceptance of the Terms of Use.