{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:12Z","timestamp":1725663372570},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540528852"},{"type":"electronic","value":"9783540471714"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_93","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:45:19Z","timestamp":1330206319000},"page":"261-275","source":"Crossref","is-referenced-by-count":7,"title":["An improved general E-unification method"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patricia","family":"Johann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"19_CR1","volume-title":"Proof Methods for Equational Theories","author":"L. Bachmair","year":"1987","unstructured":"L. Bachmair Proof Methods for Equational Theories. Dissertation, University of Illinois, Urbana Champaign, 1987."},{"key":"19_CR2","unstructured":"L. Bachmair, N. Dershowitz, and J.Hsiang. Orderings for Equational Proofs. In Proc. Symp. Logic in Computer Science, pp. 346\u2013357, 1986."},{"key":"19_CR3","unstructured":"L. Bachmair, N. Dershowitz and D. Plaisted. Completion without Failure. In Proceedings of CREAS, May 1987."},{"key":"19_CR4","unstructured":"M. Fay. First-order Unification in an Equational Theory. In Proceedings of the Fourth Workshop on Automated Deduction, Austin, Texas 1979."},{"issue":"2","key":"19_CR5","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J. H. Gallier","year":"1989","unstructured":"J. H. Gallier and W. Snyder. Complete Sets of Transformations for General E-Unification. In TCS 67:2,3, pp. 203\u2013260, 1989. Also presented at RTA, 1987.","journal-title":"TCS"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"J. Herbrand. Sur la Theorie de la Demonstration (Dissertation, 1930). In Logical Writings, W. Goldfarb, ed., Cambridge, 1971.","DOI":"10.1007\/978-94-010-3072-4"},{"key":"19_CR7","volume-title":"Formal Languages: Perspectives and Open Problems","author":"G. Huet","year":"1982","unstructured":"G. Huet and D. C. Oppen. Equations and Rewrite Rules: A Survey. In Formal Languages: Perspectives and Open Problems, R. V. Book, ed., Academic Press, NY, 1982."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"J-M. Hullot. Canonical Forms and Unification. In Proceedings of the Fifth International Conference on Automated Deduction 1980.","DOI":"10.21236\/ADA087640"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"C. Kirchner. A New Equational Unification Method: A Generalization of Martelli-Montanari's Algorithm. In Proceedings of the Seventh International Conference on Automated Deduction, 1984.","DOI":"10.1007\/978-0-387-34768-4_14"},{"key":"19_CR10","unstructured":"C. Kirchner. M\u00e9thodes et Outils de Conception Systematique d'Algorithmes d'Unification dans les Theories Equationnelles. Th\u00e8se d'Etat, Universit\u00e9 de Nancy I, 1985."},{"key":"19_CR11","unstructured":"C. Kirchner. Computing Unification Algorithms. Presented at LICS, 1986."},{"issue":"2","key":"19_CR12","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An Efficient Unificaton Algorithm. In ACM Transactions on Programming Languages and Systems 4:2, pp. 258\u2013282, 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR13","unstructured":"A. Martelli, C. Moiso, and G. F. Rossi. An Algorithm for Unification in Equational Theories. Presented at the Third Conference on Logic Programming, 1986."},{"key":"19_CR14","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building in Equational Theories. In Machine Intelligence 7, pp. 73\u201390, 1972.","journal-title":"Machine Intelligence"}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_93.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:39Z","timestamp":1605648339000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_93"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_93","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}