{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:40:03Z","timestamp":1742596803094,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569398"},{"type":"electronic","value":"9783540478263"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56939-1_107","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:56:44Z","timestamp":1330257404000},"page":"621-632","source":"Crossref","is-referenced-by-count":1,"title":["A partial solution for D-unification based on a reduction to AC 1-unification"],"prefix":"10.1007","author":[{"given":"Evelyne","family":"Contejean","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"key":"51_CR1","volume-title":"Th\u00e8se de Doctorat","author":"E. Contejean","year":"1992","unstructured":"Evelyne Contejean. \u00e9l\u00e9ments pour la d\u00e9cidabilit\u00e9 de l'unification modulo la distributivit\u00e9. Th\u00e8se de Doctorat, Universit\u00e9 de Paris-Sud, France, Avril 1992."},{"key":"51_CR2","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243\u2013309. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"51_CR3","doi-asserted-by":"crossref","unstructured":"J. Herbrand. Recherches sur la th\u00e9orie de la d\u00e9monstration. Th\u00e8se d'Etat, Univ. Paris, 1930. Also in: Ecrits logiques de Jacques Herbrand, PUF, Paris, 1968.","DOI":"10.3917\/puf.herbr.1968.01.0031"},{"issue":"3","key":"51_CR4","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/BF00243791","volume":"3","author":"A. Herold","year":"1987","unstructured":"Alexander Herold and Jorg H. Siekmann. Unification in abelian semi-groups. Journal of Automated Reasoning, 3(3):247\u2013283, 1987.","journal-title":"Journal of Automated Reasoning"},{"key":"51_CR5","volume-title":"Th\u00e8se d'Etat","author":"C. Kirchner","year":"1985","unstructured":"Claude Kirchner. M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories equationnelles. Th\u00e8se d'Etat, Univ. Nancy, France, 1985."},{"key":"51_CR6","doi-asserted-by":"crossref","unstructured":"Claude Kirchner and Francis Klay. Syntactic theories and unification. In Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia, June 1990.","DOI":"10.1109\/LICS.1990.113753"},{"key":"51_CR7","doi-asserted-by":"crossref","unstructured":"Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"51_CR8","doi-asserted-by":"crossref","unstructured":"G.S. Makanin. The problem of solvability of equations in a free semigroup. Akad. Nauk. SSSR, 233(2), 1977.","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"issue":"2","key":"51_CR9","first-page":"354","volume":"11","author":"J. V. Matijasevic","year":"1970","unstructured":"J. V. Matijasevic. Enumerable sets are diophantine. Soviet Mathematics (Dokladi), 11(2):354\u2013357, 1970.","journal-title":"Soviet Mathematics (Dokladi)"},{"issue":"1","key":"51_CR10","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"51_CR11","volume-title":"Technical Report Thesis","author":"P. Szabo","year":"1982","unstructured":"P. Szabo. Unifikationstheorie erster Ordnung. Technical Report Thesis, Fakultat fur Informatik, University Karlsruhe, Karlsruhe, West Germany, 1982."},{"key":"51_CR12","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S0747-7171(87)80026-3","volume":"3","author":"E. Tiden","year":"1987","unstructured":"Erik Tiden and Stefan Arnborg. Unification problems with one-sided distributivity. Journal of Symbolic Computation, (3):183\u2013202, 1987.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56939-1_107.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:58:13Z","timestamp":1742594293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56939-1_107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569398","9783540478263"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-56939-1_107","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}