{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T13:01:20Z","timestamp":1725627680990},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540168089"},{"type":"electronic","value":"9783642713859"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/978-3-642-71385-9_23","type":"book-chapter","created":{"date-parts":[[2011,11,2]],"date-time":"2011-11-02T10:20:41Z","timestamp":1320229241000},"page":"218-229","source":"Crossref","is-referenced-by-count":3,"title":["The Semantic Clause Graph Procedure \u2014 A First Overview"],"prefix":"10.1007","author":[{"given":"Hans J\u00fcrgen","family":"Ohlbach","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","volume-title":"Equality Reasoning Based on Graphs","author":"KH Bl\u00e4sius","year":"1986","unstructured":"Bl\u00e4sius, K.H., Equality Reasoning Based on Graphs. Ph.D.Thesis, FB. Informat\u00edik, Universit\u00e4t Kaiserslautern (1986)."},{"key":"23_CR2","volume-title":"The Sup-Inf mehtod in Presburger Arithmetic","author":"WW Bledsoe","year":"1974","unstructured":"Bledsoe, W.W., The Sup-Inf mehtod in Presburger Arithmetic. Memo ATP-18, Math.Dept., University of Texas, 1974."},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0004-3702(85)90015-3","volume":"27","author":"WW Bledsoe","year":"1985","unstructured":"Bledsoe, W.W., Kunen K., Shostak R., Completeness Results for Inequality Provers. Artificial Intelligence 27 (1985) 255\u2013288.","journal-title":"Artificial Intelligence"},{"key":"23_CR4","unstructured":"B\u00fcrckert, H.-J., Lazy Theory Unification in Prolog: An Extension of the WARREN Abstract Machine. Proc. of GWAI-86."},{"issue":"1","key":"23_CR5","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1145\/321738.321748","volume":"20","author":"JK Dixon","year":"1973","unstructured":"Dixon, J.K., Z-Resolution: Theorem Proving with Compiled Axioms, J.ACM, Vol. 20, No. 1 (1973) 127\u2013147.","journal-title":"J.ACM"},{"key":"23_CR6","unstructured":"Digricoli, V.J., Resolution by Unification and Equality, Proc. of 4th workshop on automated deduction, 179, Texas."},{"key":"23_CR7","unstructured":"Huet, G.P., Constrained Resolution: A Complete Mehtod for Higher Order Logic. Report 1117 (1972). Case Western Reserve University."},{"issue":"4","key":"23_CR8","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1145\/321906.321919","volume":"22","author":"R Kowalski","year":"1975","unstructured":"Kowalski, R., A Proof Procedure using Connection Graphs, J.ACM, Vol 22 No. 4 (1975), 424\u2013436.","journal-title":"J.ACM"},{"key":"23_CR9","volume-title":"The Markgraf Karl Refutation Procedure","author":"MGP Karl","year":"1984","unstructured":"Karl Mark G Raph: The Markgraf Karl Refutation Procedure, Bericht Memo-SEKI-MK-84\u201301 (1984), Fachbereich Informatik, Universit\u00e4t Kaiserslautern."},{"key":"23_CR10","volume-title":"North Holland","author":"D Loveland","year":"1978","unstructured":"Loveland, D., Automated Theorem Proving, North Holland, (1978)."},{"key":"23_CR11","unstructured":"Morris, J.B., E-resolution: An extension of Resolution to include the Equality Relation, Proc. of IJCAI (1969), 287\u2013294."},{"issue":"2","key":"23_CR12","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C., Fast decision procedures based on congruence closure. J.ACM 27, 2 (1980), 356\u2013364.","journal-title":"J.ACM"},{"issue":"1","key":"23_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A., A Machine Oriented Logic Based on the Resolution Principle, J.ACM, Vol. 12, No. 1 (1965), 23\u201341.","journal-title":"J.ACM"},{"key":"23_CR14","volume-title":"The Markgraf Karl Refutation Procedure: The Logic Engine","author":"HJ Ohlbach","year":"1982","unstructured":"Ohlbach, HJ., The Markgraf Karl Refutation Procedure: The Logic Engine. Interner Bericht 24\/82 (1982), Inst. f. Informatik I, Univ. of Karlsruhe."},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Ohlbach, HJ., Link Inheritance in Abstract Clause Graphs, Journal of Automated Reasoning (1986) (forthcoming).","DOI":"10.1007\/978-3-642-71145-9_6"},{"key":"23_CR16","unstructured":"Ohlbach, HJ., The Semantic Clause Graph Calculus, Ph.D.Thesis, FB. Informatik, University of Kaiserslautern (in preparation)."},{"key":"23_CR17","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"RE Shostak","year":"1976","unstructured":"Shostak, R.E., Refutation Graphs. Artificial Intelligence 7 (1976) 51\u201364.","journal-title":"Artificial Intelligence"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Siekmann, J., Universal Unification, Proc. of 7th CADE, Napa (1984), 1\u201342, Lecture Notes in Computer Science, Springer.","DOI":"10.1007\/978-0-387-34768-4_1"},{"issue":"4","key":"23_CR19","first-page":"333","volume":"1","author":"ME Stickel","year":"1985","unstructured":"Stickel, M.E., Automated Deduction by Theory Resolution., J.AR, Vol 1, No. 4 (1985), 333\u2013356.","journal-title":"J.AR"},{"key":"23_CR20","volume-title":"Karlsruhe","author":"L Wos","year":"1983","unstructured":"Wos, L, Automated Reasoning: Real Uses and Potential Uses. Proc. of 8th UCAI, Karlsruhe (1983)."},{"key":"23_CR21","volume-title":"Automated Reasoning - Introduction and Applications","author":"L Wos","year":"1984","unstructured":"Wos, L, Overbeek,R., Lusk, E., Boye, J., Automated Reasoning - Introduction and Applications, Prentice-Hall, Englewood Cliffs, NJ (1984)."}],"container-title":["Informatik-Fachberichte","GWAI-86 und 2. \u00d6sterreichische Artificial-Intelligence-Tagung"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-71385-9_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:12:13Z","timestamp":1606259533000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-71385-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540168089","9783642713859"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-71385-9_23","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1986]]}}}