{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:39Z","timestamp":1749124059552},"publisher-location":"Berlin\/Heidelberg","reference-count":15,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540571841"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0022569","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T01:14:45Z","timestamp":1131844485000},"page":"202-210","source":"Crossref","is-referenced-by-count":6,"title":["A rule-based algorithm for rigid E-unification"],"prefix":"10.1007","author":[{"given":"Jean","family":"Goubault","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"23_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. Andrews","year":"1981","unstructured":"P. Andrews. Theorem proving via general matings. J. ACM, 28(2):193\u2013214, April 1981.","journal-title":"J. ACM"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair, N. Dershowitz, and D. Plaisted. Completion without failure. In Resolution of Equations in Algebraic Structures, volume 2, pages 1\u201330. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"23_CR3","unstructured":"B. Beckert. A completion-based method for adding equality to free variable semantic tableaux. In Workshop on Theorem Proving with Analytic. Tableaux and Related Methods, number MPI-I-93-213, pages 19\u201322, Marseille, France, avril 1993."},{"key":"23_CR4","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0304-3975(79)90054-9","volume":"8","author":"W. Bibel","year":"1979","unstructured":"W. Bibel. Tautology testing with a generalized matrix reduction method. Theoretical Computer Science, 8:31\u201344, 1979.","journal-title":"Theoretical Computer Science"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, 2nd, revised edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"issue":"4","key":"23_CR6","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P. K. Downey","year":"1980","unstructured":"P. K. Downey, R. Sethi, and R. E. Tarjan. Variations on the common subexpression problem. J. ACM, 27(4):758\u2013771, 1980.","journal-title":"J. ACM"},{"key":"23_CR7","unstructured":"J. Gallier. Logic for Computer Science \u2014 Foundations of Automatic Theorem Proving. John Wiley and Sons, 1987."},{"issue":"2","key":"23_CR8","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/128749.128754","volume":"39","author":"J. Gallier","year":"1992","unstructured":"J. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. J. ACM, 39(2):377\u2013429, April 1992.","journal-title":"J. ACM"},{"key":"23_CR9","unstructured":"J. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification equational matings. In LICS, pages 338\u2013346. IEEE, 1987."},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"J. Gallier, W. Snyder, P. Narendran, and D. Plaisted. Rigid E-unification is NP-complete. In LICS, pages 218\u2013227. IEEE, 1988.","DOI":"10.1109\/LICS.1988.5121"},{"key":"23_CR11","unstructured":"J. Goubault. D\u00e9monstration automatique en logique classique: complexit\u00e9 et m\u00e9thodes. PhD thesis, Laboratoire d'informatique de l'\u00e9cole polytechnique, 1993."},{"key":"23_CR12","unstructured":"J. Goubault. A rule-based algorithm for rigid E-unification. Technical Report 93024, Bull S.A., juin 1993."},{"key":"23_CR13","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. Technical report, LRI, CNRS UA 410, March 1990."},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"K. Mehlhorn and A. Tsakalidis. Data structures. In J. v. Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 301\u2013341. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88071-0.50011-4"},{"issue":"2","key":"23_CR15","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. G. Oppen. Fast decision procedures based on congruence closure. J. ACM, 27(2):356\u2013364, April 1980.","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022569.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T16:49:05Z","timestamp":1607532545000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022569"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540571841"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0022569","relation":{},"subject":[]}}