{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:49Z","timestamp":1725456229350},"publisher-location":"Berlin\/Heidelberg","reference-count":36,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012846","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T01:12:39Z","timestamp":1132708359000},"page":"397-414","source":"Crossref","is-referenced-by-count":0,"title":["Partial unification for graph based equational reasoning"],"prefix":"10.1007","author":[{"given":"Karl Hans","family":"Bl\u00e4sius","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00f6rg H.","family":"Siekmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"R. Anderson: Completeness results for E-resolution, Proc. Spring Joint Conf., 653\u2013656, 1970","DOI":"10.1145\/1476936.1477034"},{"key":"27_CR2","unstructured":"K.H. Bl\u00e4sius, N. Eisinger, J. Siekmann, G. Smolka, A. Herold, C. Walther: The Markgraf Karl Refutation Procedure, Proc. IJCAI, 511\u2013518, 1981"},{"key":"27_CR3","unstructured":"K.H. Bl\u00e4sius: Equality Reasoning in Clause Graphs, Proc. IJCAI, 936\u2013939, 1983"},{"key":"27_CR4","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/978-3-642-71385-9_24","volume":"124","author":"K.H. Bl\u00e4sius","year":"1986","unstructured":"K.H. Bl\u00e4sius: Against the \u2018Anti Waltz Effect\u2019 in Equality Reasoning, Proc. German Workshop on Artificial Intelligence, Informatik-Fachberichte 124, Springer, 230\u2013241, 1986","journal-title":"Proc. German Workshop on Artificial Intelligence, Informatik-Fachberichte"},{"key":"27_CR5","unstructured":"K.H. Bl\u00e4sius: Equality Reasoning Based on Graphs, SEKI-REPORT SR-87-01 (Ph.D. thesis), Fachbereich Informatik, Universit\u00e4t Kaiserslautern, 1987"},{"key":"27_CR6","unstructured":"R.S. Boyer, J.S. Moore: The Sharing of Structure in Theorem-proving Programs, Machine Intelligence 7, Edinburgh University Press, 101\u2013116, 1972"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"D. Brand: Proving Theorems with the Modification Method, SIAM Journal of Comp., vol 4, No. 4, 1975","DOI":"10.1137\/0204036"},{"issue":"1","key":"27_CR8","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(87)80020-2","volume":"3","author":"B. Buchberger","year":"1987","unstructured":"B. Buchberger: History and Basic Features of the Critical-Pair\/Completion Procedure, Journal of Symbolic Computation, Vol. 3, Nos 1 & 2, 3\u201338, 1987","journal-title":"Journal of Symbolic Computation"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert: Lazy Theory Unification in Prolog: An Extension of the Warren Abstract Machine, Proc. GWAI-86, IFB 124, Springer Verlag, 277\u2013289, 1986","DOI":"10.1007\/978-3-642-71385-9_28"},{"key":"27_CR10","unstructured":"V.J. Digricoli: Resolution by Unification and Equality, Proc. 4th Workshop on Automated Deduction, Texas, 1979"},{"key":"27_CR11","unstructured":"V.J. Digricoli: The Management of Heuristic Search in Boolean Experiments with RUE-resolution, Proc. IJCAI-85, Los Angeles, 1985"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"G. Huet, D. Oppen: Equations and Rewrite Rules: A survey, Technical Report CSL-111, SRI International, 1980","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"27_CR13","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"R. Kowalski: A Proof Procedure Using Connection Graphs, JACM 22, 4, 1975","journal-title":"JACM"},{"key":"27_CR14","volume-title":"Proc. of Colloq. on Equations in Algebraic Structures","author":"C. Kirchner","year":"1987","unstructured":"C. Kirchner: Methods and Tools for Equational Unification, Proc. of Colloq. on Equations in Algebraic Structures, Lakeway, Texas, 1987"},{"key":"27_CR15","unstructured":"Y. Lim, L.J. Henschen: A New Hyperparamodulation Strategy for the Equality Relation, Proc. IJCAI-85, Los Angeles, 1985"},{"key":"27_CR16","first-page":"232","volume":"87","author":"E.L. Lusk","year":"1980","unstructured":"E.L. Lusk, R.A. Overbeek: Data Structures and Control Architecture for Implementation of Theorem-Proving Programs, Proc. 5th CADE, Springer Lecture Notes, vol. 87, 232\u2013249, 1980","journal-title":"Proc. 5th CADE, Springer Lecture Notes"},{"key":"27_CR17","unstructured":"J.B. Morris: E-resolution: An Extension of Resolution to include the Equality Relation, Proc. IJCAI, 1969, 287\u2013294"},{"key":"27_CR18","unstructured":"W. Nutt, P. Rety, G. Smolka: Basic Narrowing Revisted, SEKI-Report SR-87-7, Univ. of Kaiserslautern, 1987; to appear in J. of Symbolic Computation, 1988"},{"key":"27_CR19","unstructured":"A. Newell, J.C. Shaw, H. Simon: Report on a General Problem Solving Program, Proc. Int. Conf. Information Processing (UNESCO). Paris, 1959"},{"key":"27_CR20","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D. Plaisted","year":"1981","unstructured":"D. Plaisted: Theorem Proving with Abstraction, Artifical Intelligence 16, 47\u2013108, 1981","journal-title":"Artifical Intelligence"},{"key":"27_CR21","unstructured":"A. Pr\u00e4cklein: Equality Reasoning, Internal Working Paper, Univ. of Kaiserslautern, 1987"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"M. Richter: Logik Kalk\u00fcle, Teubner Verlag, 1978","DOI":"10.1007\/978-3-322-91208-4"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"J.A. Robinson: A Machine-Oriented Logic Based on the Resolution Principle, JACM 12, 1965","DOI":"10.1145\/321250.321253"},{"key":"27_CR24","unstructured":"M. Rusinowitch: D\u00e9monstration Automatique par des Techniques de R\u00e9\u00e9criture, Th\u00e8se d'\u00e9tat, CRIN, Centre de Recherche en Informatique de Nancy, 1987"},{"key":"27_CR25","first-page":"135","volume":"4","author":"G. Robinson","year":"1969","unstructured":"G. Robinson, L. Wos: Paramodulation and TP in first order theories with equality, Machine Intelligence 4, 135\u2013150, 1969","journal-title":"Machine Intelligence"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"R.E. Shostak: An Algorithm for Reasoning About Equality, CACM, vol 21, no. 7, 1978","DOI":"10.1145\/359545.359570"},{"key":"27_CR27","first-page":"103","volume":"4","author":"E.E. Sibert","year":"1969","unstructured":"E.E. Sibert: A machine-oriented Logic incorporating the Equality Axiom, Machine Intelligence, vol 4, 103\u2013133, 1969","journal-title":"Machine Intelligence"},{"key":"27_CR28","unstructured":"J. Siekmann: Unification Theory, Proc. of European Conf. on Artificial Intelligence (ECAI), 1986 full paper to appear in J. of Symbolic Computation, 1988"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"G. Smolka, W. Nutt, J. Goguen, J. Meseguer: Order-sorted equational computation, in M. Nivat, H. Ait-Kaci (eds): Resolving Equational Systems, Addison-Wesley, to appear 1988","DOI":"10.1016\/B978-0-12-046371-8.50016-X"},{"issue":"4","key":"27_CR30","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"M. Stickel: Automated Deduction by Theory Resolution, Journal of Automated Reasoning Vol. 1, No. 4 (1985), 333\u2013356","journal-title":"Journal of Automated Reasoning"},{"key":"27_CR31","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/BF00288537","volume":"13","author":"J. Siekmann","year":"1980","unstructured":"J. Siekmann, G. Wrightson: Paramodulated Connectiongraphs, Acta Informatica 13, 67\u201386, 1980","journal-title":"Acta Informatica"},{"key":"27_CR32","volume-title":"Equational Logic and Equational Theories of Algebra","author":"A. Tarski","year":"1986","unstructured":"A. Tarski: Equational Logic and Equational Theories of Algebra, in: Schmidt et.al. (eds): Contribution to Mathematical Logic, North Holland, 1986"},{"key":"27_CR33","unstructured":"W. Taylor: Equational Logic, Houston Journal of Maths, 5, 1979"},{"key":"27_CR34","unstructured":"D.H.D. Warren: An Abstract Prolog Instruction Set, SRI Technical Note 309, Sri International, October 1983"},{"key":"27_CR35","unstructured":"L. Wos, R. Overbeek, E. Lusk, J. Boyle: Automated Reasoning, Introduction and Applications, Prentice Hall, 1984"},{"key":"27_CR36","doi-asserted-by":"publisher","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L. Wos","year":"1967","unstructured":"L. Wos, G. Robinson, D. Carson, L. Shalla: The Concept of Demodulation in Theorem Proving, J. ACM 14, 698\u2013709, 1967","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012846","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:25:36Z","timestamp":1586564736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012846"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/bfb0012846","relation":{},"subject":[]}}