摘要:
springer.com 
sci-hub.st 参考文章(6)
J. A. Robinson, Theorem-Proving on the Computer Journal of the ACM. ,vol. 10, pp. 163- 174 ,(1963) , 10.1145/321160.321166
Martin Davis, Hilary Putnam, A Computing Procedure for Quantification Theory Journal of the ACM. ,vol. 7, pp. 201- 215 ,(1960) , 10.1145/321033.321034
Joyce Friedman, A Semi-Decision Procedure for the Functional Calculus Journal of the ACM. ,vol. 10, pp. 1- 24 ,(1963) , 10.1145/321150.321151
P. C. Gilmore, A proof method for quantification theory: its justification and realization Ibm Journal of Research and Development. ,vol. 4, pp. 28- 35 ,(1960) , 10.1147/RD.41.0028
J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle Journal of the ACM. ,vol. 12, pp. 23- 41 ,(1965) , 10.1145/321250.321253
Lawrence Wos, Daniel Carson, George Robinson, The unit preference strategy in theorem proving Proceedings of the October 27-29, 1964, fall joint computer conference, part I on XX - AFIPS '64 (Fall, part I). pp. 615- 621 ,(1964) , 10.1145/1464052.1464109