
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 475486, October, 1992.  
BibTex  x  
@article{ 10.1109/69.166989, author = {M.Y. Fang and W.T. Chen}, title = {Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers}, journal ={IEEE Transactions on Knowledge and Data Engineering}, volume = {4}, number = {5}, issn = {10414347}, year = {1992}, pages = {475486}, doi = {http://doi.ieeecomputersociety.org/10.1109/69.166989}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Knowledge and Data Engineering TI  Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers IS  5 SN  10414347 SP475 EP486 EPD  475486 A1  M.Y. Fang, A1  W.T. Chen, PY  1992 KW  vectorisation; deduction rules; theorem proving; propositional logic; vector computers; artificial intelligence; formal logic; theorem proving; vector processor systems VL  4 JA  IEEE Transactions on Knowledge and Data Engineering ER   
Vectorization techniques for solving the theoremproving 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. II229II235.
[3] W. T. Chen and L. L. Liu, "Parallel approach for theorem proving in propositional logic,"Inform. Sci., vol. 41, no. 1, pp. 6176, 1987.
[4] S. A. Cook, "The complexity of theoremproving procedures," inProc. 3rd Annu. ACM Symp. Theory of Comput., 1971, pp. 151158.
[5] M. Davis and H. Putnam, "A computing procedure for quantification theory,"J. Ass. Comput. Mach., vol. 7, no. 3, pp. 201215, 1960.
[6] M. R. Garey and D. S. Johnson,Computers and Intractability: A Guide to Theory of NPCompleteness. San Francisco, CA: Freeman, 1979.
[7] K. Hwang and F. A. Briggs,Computer Architecture and Parallel Processing. New York: McGrawHill, 1984.
[8] K. Hwang, "Multiprocessor supercomputers for scientific engineering application,"Comput., vol. 18, no. 6, pp. 5773, June 1985.
[9] D. W. Loveland,Automated Theorem Proving: A Logic Basis. Amsterdam, The Netherlands: NorthHolland, 1978.
[10] D. W. Loveland, "Automated theorem proving: A quarter century review,"Contemporary Math., vol. 29, pp. 145, 1984.
[11] Scientific Supercomputer Subcommittee, "Software for supercomputers,"Computer, vol. 21, no. 12, pp. 7074, Dec. 1988.
[12] A. Urquhart, "Hard examples for resolution,"J. Ass. Comput. Mach., vol. 31, no. 1, pp. 209219, 1987.