{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T13:42:14Z","timestamp":1648734134822},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/bf00881913","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T20:34:58Z","timestamp":1104006898000},"page":"83-115","source":"Crossref","is-referenced-by-count":0,"title":["On the termination of clause graph resolution"],"prefix":"10.1007","volume":"13","author":[{"given":"C. A.","family":"Johnson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1145\/321466.321469","volume":"15","author":"P. B. Andrews","year":"1968","unstructured":"Andrews, P. B. (1968): Resolution with merging,J. ACM 15, 367?381.","journal-title":"J. ACM"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"801","DOI":"10.1109\/TC.1976.1674698","volume":"C-25","author":"P. B. Andrews","year":"1976","unstructured":"Andrews, P. B. (1976): Refutations by mating,IEEE Trans. Computing C-25, 801?807.","journal-title":"IEEE Trans. Computing"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. B. Andrews","year":"1981","unstructured":"Andrews, P. B. (1981): Theorem proving via general mating,J. ACM 28, 193?214.","journal-title":"J. ACM"},{"key":"CR4","unstructured":"Baader, F. (1991): Unification, weak unification, upper bound, lower bound and generalization problems, inProc. Rewriting Techniques and Applications, Springer LNCS 488, 86?97."},{"key":"CR5","unstructured":"Bibel, W. (1980):A Strong Completeness Result for the Connection Graph Proof Procedure, Bericht ATP-3-IV-80, Institut f\u00fcr Informatik, Technische Univ., M\u00fcnchen."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W. (1981): On matrices with connections,J. ACM 28, 633?645.","journal-title":"J. ACM"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Bibel, W. (1981): On the completeness of connection graph resolution,Proc. GWAI-81, Springer Informatik Fachberichte, vol. 47, J. H. Siekmann (ed.), 246?247.","DOI":"10.1007\/978-3-662-02328-0_22"},{"key":"CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1987","unstructured":"Bibel, W. (1987):Automated Theorem Proving, Vieweg, Wiesbaden."},{"key":"CR9","volume-title":"The inheritance of links in a clause graph, Report CW2","author":"M. Bruynooghe","year":"1975","unstructured":"Bruynooghe, M. (1975): The inheritance of links in a clause graph, Report CW2, Applied Mathematics and Programming Division, Katholieke Universiteit, Leuven."},{"key":"CR10","volume-title":"Classical Papers on Computational Logic 1957?1966","author":"M. Davis","year":"1983","unstructured":"Davis, M. (1983): The prehistory and early history of automated deduction, in I. Siekmann and G. Wrightson (eds.),Classical Papers on Computational Logic 1957?1966, Springer, Heidelberg."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Derschowitz","year":"1987","unstructured":"Derschowitz, N. (1987): Termination of rewriting,J. Symbolic Computation 3, 69?116.","journal-title":"J. Symbolic Computation"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/S0747-7171(85)80027-4","volume":"1","author":"E. Eder","year":"1985","unstructured":"Eder, E. (1985): Properties of substitutions and unifications,J. Symbolic Computation 1, 31?46.","journal-title":"J. Symbolic Computation"},{"key":"CR13","unstructured":"Eisinger, N. (1986): What you always wanted to know about clause graph resolution, inProc. 8th CADE, Springer LNCS 230, 316?336."},{"key":"CR14","volume-title":"Completeness, Confluence and Related Properties of Clause Graph Resolution","author":"N. Eisinger","year":"1991","unstructured":"Eisinger, N. (1991):Completeness, Confluence and Related Properties of Clause Graph Resolution, Pitman, London."},{"key":"CR15","unstructured":"Goldberg, A. (1979): Average complexity of the satisfiability problem, in W. Joyner (ed.),Proc. 4th Workshop on Automated Deduction, Austin, Texas, pp. 1?16."},{"key":"CR16","unstructured":"Herold, A. (1983):Some Basic Notions of First-Order Unification Theory, Internal Report 15\/83, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe."},{"key":"CR17","unstructured":"Johnson, C. (1993):On the Termination of Clause Graph Resolution, preprint."},{"key":"CR18","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D. and Bendixson, D. (1970): Simple word problems in universal algebras, in J. Leech (ed.),Computational Problems in Abstract Algebra, Pergamon Press, London, pp. 263?297."},{"key":"CR19","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R. Kowalski","year":"1971","unstructured":"Kowalski, R. and Kuehner, D. (1971): Linear resolution with selection function,Artificial Intelligence 2, 227?260.","journal-title":"Artificial Intelligence"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"Kowalski, R. (1975): A proof procedure using connection graphs,J. ACM 22, 572?595.","journal-title":"J. ACM"},{"key":"CR21","volume-title":"Logic for Problem Solving","author":"R. Kowalski","year":"1979","unstructured":"Kowalski, R. (1979):Logic for Problem Solving, North-Holland, Amsterdam."},{"key":"CR22","volume-title":"Automated Theorem Proving","author":"D. Loveland","year":"1978","unstructured":"Loveland, D. (1978):Automated Theorem Proving, North-Holland, Amsterdam."},{"key":"CR23","volume-title":"Problem Solving Methods in Artificial Intelligence","author":"N. J. Nilsson","year":"1971","unstructured":"Nilsson, N. J. (1971):Problem Solving Methods in Artificial Intelligence, McGraw-Hill, New York."},{"key":"CR24","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"Robinson, J. (1965): A machine orientated logic based on the resolution principle,J. ACM 12, 23?41.","journal-title":"J. ACM"},{"key":"CR25","first-page":"151","volume":"4","author":"J. Robinson","year":"1969","unstructured":"Robinson, J. (1969): Mechanizing higher order logic,Machine Intelligence 4, 151?170.","journal-title":"Machine Intelligence"},{"key":"CR26","first-page":"63","volume":"6","author":"J. Robinson","year":"1971","unstructured":"Robinson, J. (1971): Computational logic: The Unification Computation,Machine Intelligence 6, 63?72.","journal-title":"Machine Intelligence"},{"key":"CR27","unstructured":"Noll, H. (1980): A note on resolution: How to get rid of factoring without losing completeness,Proc. 5th CADE, Springer LNCS 87, 250?263."},{"key":"CR28","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(08)80130-7","volume":"11","author":"J. Pais","year":"1991","unstructured":"Pais, J. and Peterson, G. (1991): Using forcing to prove completeness of resolution and paramodulation,J. Symbolic Computation 11, 3?19.","journal-title":"J. Symbolic Computation"},{"key":"CR29","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. Peterson","year":"1983","unstructured":"Peterson, G. (1983): A technique for establishing completeness results in theorem proving with equality,SIAM J. Computing 12, 82?100.","journal-title":"SIAM J. Computing"},{"key":"CR30","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R. E. Shostak","year":"1976","unstructured":"Shostak, R. E. (1976): Refutation graphs,Artificial Intelligence 7, 51?64.","journal-title":"Artificial Intelligence"},{"key":"CR31","unstructured":"Shostak, R. E. (1979):A Graph Theoretic View of Resolution Theorem Proving, Report SRI Int., Menlo Park, Calif."},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"Smolka, G. (1982): Completeness of the connection graph proof procedure for unit refutable clause sets,Proc. GWAI-82, Springer Informatik Fachberichte, vol. 58, pp. 191?204.","DOI":"10.1007\/978-3-642-68826-3_14"},{"key":"CR33","series-title":"Full version as Int. Ber.","first-page":"40","volume-title":"AISB\/GI Conf. on Artificial Intelligence","author":"W. Stephen","year":"1978","unstructured":"Stephen, W. and Siekmann, J. (1978): Completeness and soundness of the connection graph proof procedure, inAISB\/GI Conf. on Artificial Intelligence, D. Sleeman (ed.), Leeds Univ. Press, pp. 40?344. Full version as Int. Ber. 7\/76, Institut f\u00fcr Informatik, Univ., Karlsruhe."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881913.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881913\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881913","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T12:58:11Z","timestamp":1556542691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881913"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881913"],"URL":"https:\/\/doi.org\/10.1007\/bf00881913","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}