{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T03:17:19Z","timestamp":1649128639251},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1980,1,1]],"date-time":"1980-01-01T00:00:00Z","timestamp":315532800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1980,1]]},"DOI":"10.1007\/bf00288537","type":"journal-article","created":{"date-parts":[[2004,10,4]],"date-time":"2004-10-04T15:11:38Z","timestamp":1096902698000},"page":"67-86","source":"Crossref","is-referenced-by-count":7,"title":["Paramodulated connection graphs"],"prefix":"10.1007","volume":"13","author":[{"given":"J\ufffdrg","family":"Siekmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Graham","family":"Wrightson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.2307\/1970103","volume":"70","author":"W.W. Boone","year":"1959","unstructured":"Boone, W.W.: The Word Problem. Ann. Math. 70, 207?265 (1959)","journal-title":"Ann. Math."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Brand, D.: Proving Theorems with the Modification Method. SIAM J. Comp. 4 (1975)","DOI":"10.1137\/0204036"},{"key":"CR3","unstructured":"Brown, F.M.: Notes on Chains and Connection Graphs. Personal Notes. Dept. Computational Logic, University of Edinburgh, 1976"},{"key":"CR4","unstructured":"Bruynooghe, M.: The Inheritance of Links in a Connection Graph. Report CW7, Applied Mathematics and Programming Division, Katholieke Universiteit Leuven, 1975"},{"key":"CR5","unstructured":"Daniels, S., Livesay, M., Mathis, C.H., Raulefs, P., Siekmann, J., Stephan, W., Unvericht, E., Wrightson, G.: Incorporating Mathematical Knowledge into an Automatic Theorem Proving System investigated for the Case of Automata Theory, I. Interner Bericht Nr. 6\/77, Institut f\u00fcr Informatik I, Universit\u00e4t Karlsruhe, 1977"},{"key":"CR6","unstructured":"Eisinger, N., Siekmann, J., Unvericht, E.: The Markgraf Karl Refutation Procedure. Interner Bericht, Institut f\u00fcr Informatik I, Universit\u00e4t Karlsruhe, 1979"},{"key":"CR7","unstructured":"Kowalski, R.: Logic for Problem-Solving. Memo 75, University of Edinburgh, 1974"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Kowalski, R.: A Proof Procedure Using Connection Graphs. JACM 22 (1975)","DOI":"10.1145\/321906.321919"},{"key":"CR9","unstructured":"Ballantyne, A.M., Lankford, D.: Decision Procedures for Simple Equational Theories. University of Texas at Austin, ATP-35, ATP-37, ATP-39, 1977"},{"key":"CR10","unstructured":"Richter, M.M.: A Note on Paramodulation and the Functional Reflexive Axioms. Institut f\u00fcr Informatik, Universit\u00e4t Aachen, Templergraben 35, 1975"},{"key":"CR11","volume-title":"Machine Intelligence 4","author":"G.A. Robinson","year":"1969","unstructured":"Robinson, G.A., Wos, L.: Paramodulation and Theorem Proving in First Order Theories with Equality. In: Machine Intelligence 4 (B. Meltzer and D. Michie, eds.), New York: American Elsevier 1969"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. JACM 12 (1965)","DOI":"10.1007\/978-3-642-81952-0_26"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Shostak, R.E.: Refutation Graphs. Journal of Artificial Intelligence 7 (1976)","DOI":"10.1016\/0004-3702(76)90021-7"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Sickel, S.: Clause Interconnectivity Graphs, IEEE Trans. on Computing, C-25 (1976)","DOI":"10.1109\/TC.1976.1674701"},{"key":"CR15","unstructured":"Siekmann, J., Stephan, W.: Completeness and Consistency of the Connection Graph Proof Procedure. Interner Bericht Nr. 7\/76, Institut f\u00fcr Informatik I, Universit\u00e4t Karlsruhe, 1976"},{"key":"CR16","unstructured":"Siekmann, J., Wrightson, G.: Paramodulated Connection Graphs. Interner Bericht Nr. 5\/77, Institut f\u00fcr Informatik I, Universit\u00e4t Karlsruhe, 1977"},{"key":"CR17","unstructured":"Waltz, D.L.: Generating Semantic Descriptions from Drawings of Scenes with Shadows. Ph. D., MIT, AI-Lab., 1972"},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"Wos, L., Robinson, G.: Maximal Models and Refutation Completeness: Semidecision Procedures in Automatic Theorem Proving. In: Wordproblems (W.W. Boone, F.B. Cannonito, R.C. Lyndon, eds.), North-Holland, 1973","DOI":"10.1016\/S0049-237X(08)71923-2"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Yates, R.A., Raphael, B., Hart, T.P.: Resolution Graphs. Journal of Artificial Intelligence 1 (1970)","DOI":"10.1016\/0004-3702(70)90011-1"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00288537.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00288537\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00288537","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:58:56Z","timestamp":1585900736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00288537"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1980,1]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1980,1]]}},"alternative-id":["BF00288537"],"URL":"https:\/\/doi.org\/10.1007\/bf00288537","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1980,1]]}}}