Subsumption, a Sometimes Undervalued Procedure

作者: Argonne National Laboratory. Mathematics and Computer Science Division

DOI:

关键词:

摘要: Rarely do circumstances permit one to simultaneously acknowledge a colleague's contributions, evaluate the relative importance of basic elements field, and compare various paradigms for attacking class problems. However, through fortuitous set occurrences, we have that opportunity. We shall, therefore, take full advantage situation by presenting an evaluation J. A. Robinson's contribution

参考文章(21)
J. A. Robinson, Automatic Deduction with Hyper-Resolution Springer Berlin Heidelberg. pp. 416- 423 ,(1983) , 10.1007/978-3-642-81952-0_27
L. Wos, R. Veroff, B. Smith, W. McCune, The Linked Inference Principle, II: The User's Viewpoint conference on automated deduction. pp. 316- 332 ,(1984) , 10.1007/978-0-387-34768-4_19
Lawrence Wos, George A. Robinson, Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving Journal of the ACM. ,vol. 12, pp. 536- 541 ,(1965) , 10.1145/321296.321302
Mark E. Stickel, A Prolog technology theorem prover: implementation by an extended Prolog computer Journal of Automated Reasoning. ,vol. 4, pp. 353- 380 ,(1988) , 10.1007/BF00297245
J. R. Guard, F. C. Oglesby, J. H. Bennett, L. G. Settle, Semi-Automated Mathematics Journal of the ACM. ,vol. 16, pp. 49- 62 ,(1969) , 10.1145/321495.321500
DavidA. Plaisted, Non-horn clause logic programming without contrapositives Journal of Automated Reasoning. ,vol. 4, pp. 287- 325 ,(1988) , 10.1007/BF00244944
L. Wos, S. Winker, R. Veroff, B. Smith, L. Henschen, Questions concerning possible shortest single axioms for the equivalential calculus: an application of automated theorem proving to infinite domains Notre Dame Journal of Formal Logic. ,vol. 24, pp. 205- 223 ,(1983) , 10.1305/NDJFL/1093870311
L. Wos, Steve Winker, Automated generation of models and counterexamples and its application to open questions in Ternary Boolean algebra international symposium on multiple-valued logic. pp. 251- 256 ,(1978) , 10.5555/800129.804214