{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T01:38:46Z","timestamp":1649122726997},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[1988,12,1]],"date-time":"1988-12-01T00:00:00Z","timestamp":596937600000},"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":[[1988,12]]},"DOI":"10.1007\/bf00297248","type":"journal-article","created":{"date-parts":[[2004,10,6]],"date-time":"2004-10-06T07:01:18Z","timestamp":1097046078000},"page":"425-444","source":"Crossref","is-referenced-by-count":4,"title":["A new reduction rule for the connection graph proof procedure"],"prefix":"10.1007","volume":"4","author":[{"given":"Klaus Heje","family":"Munch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W., ?On Matrices with Connections.? J ACM 28, 633?545 (1981).","journal-title":"J ACM"},{"key":"CR2","unstructured":"Bl\u00e4sius, K., Eisinger, N., Siekman, J., Smolka, G., Herold, A., and Walther, C., The Markgraph Karl Refutation Procedure (Fall 1981). Proc. of the Seventh Int. Joint Conf. on Artificial Intelligence, Vancouver, BC, Canada, pp. 511?518 (1981)."},{"key":"CR3","unstructured":"Boyer, R. S., Locking: a Restriction of Resolution. PhD dissertation, University of Texas, Austin, Texas (1971)."},{"key":"CR4","unstructured":"Bruynooghe, M., The inheritance of links in a connection graph. Report CW2. Applied Mathematics and Programming Division. Katholieke Universiteit Leuven (1975)."},{"key":"CR5","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"Chang, C., and Lee, R. C., Symbolic Logic and Mechanical Theorem Proving. Academic Press, London (1973)."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Eisinger, N., ?What You Always Wanted to Know about Clause Graph Resolution.? 8th Int. Conf. on Automated Deduction, Oxford, England, pp. 316?336 (July 1986).","DOI":"10.1007\/3-540-16780-3_100"},{"key":"CR7","first-page":"37","volume-title":"Fundamentals of Artificial Intelligence","author":"G. Huet","year":"1985","unstructured":"Huet, G., ?Deduction and Computation.? In Fundamentals of Artificial Intelligence, eds. W.Bibel and Ph.Jorrand, Springer, Berlin, 37?74 (1985)."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"Kowalski, R., ?A Proof Procedure Using Connection Graphs.? J ACM 22, 572?595 (1975).","journal-title":"J ACM"},{"key":"CR9","series-title":"Artificial Intelligence Series","volume-title":"Logic for Problem Solving","author":"R. Kowalski","year":"1979","unstructured":"Kowalski, R., Logic for Problem Solving. Artificial Intelligence Series. Vol. 7, North-Holland, New York (1979)."},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Smolka, G. Completeness of the Connection Graph Proof Procedure for Unit-Refutable Clause Sets. GWAI-82, 6th German Workshop on Artificial Intelligence, Bad Honnef, pp. 191?204 (Sept. 1982).","DOI":"10.1007\/978-3-642-68826-3_14"},{"key":"CR11","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"Stickel, M., Automated Deduction by Theory Resolution. Journal of Automated Reasoning, 1 333?355 (1985).","journal-title":"Journal of Automated Reasoning"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF00246025","volume":"2","author":"M. Stickel","year":"1986","unstructured":"Stickel, M., ?Schubert's Steamroller Problem: Formulations and Solutions.? Journal of Automated Reasoning, 2, 89?101 (1986).","journal-title":"Journal of Automated Reasoning"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0004-3702(85)90029-3","volume":"26","author":"C. Walther","year":"1985","unstructured":"Walther, C., ?A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution.? Journal of Artificial Intelligence, 26, 217?224 (1985).","journal-title":"Journal of Artificial Intelligence"},{"key":"CR14","unstructured":"Walther, C., ?A Many-Sorted Calculus Based on Resolution and Paramodulation.? Proc. of the Eighth Int. Joint Conf. on Artificial Intelligence, Karlsruhe, pp. 882?891 (1983)."},{"key":"CR15","doi-asserted-by":"crossref","first-page":"835","DOI":"10.1109\/TC.1976.1674702","volume":"25","author":"S. Winker","year":"1976","unstructured":"Winker, S., ?An Evaluation of an Implementation of Qualified Hyperresolution.? IEEE Transactions on Computers C-25, pp. 835?843 (1976).","journal-title":"IEEE Transactions on Computers"},{"key":"CR16","unstructured":"Wos, L., Veroff, R., Smith, B., and McCune, W., ?The Linked Inference Principle, II: The user's viewpoint.? Proc. of the 7th Int. Conf. on Automated Deduction, Napa, California, pp. 316?332 (1984)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00297248.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00297248\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00297248","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T16:12:53Z","timestamp":1554739973000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00297248"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,12]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1988,12]]}},"alternative-id":["BF00297248"],"URL":"https:\/\/doi.org\/10.1007\/bf00297248","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988,12]]}}}