{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:50:00Z","timestamp":1725475800821},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_17","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T16:12:31Z","timestamp":1167408751000},"page":"220-234","source":"Crossref","is-referenced-by-count":4,"title":["Rigid E-Unification Revisited"],"prefix":"10.1007","author":[{"given":"Ashish","family":"Tiwari","sequence":"first","affiliation":[]},{"given":"Leo","family":"Bachmair","sequence":"additional","affiliation":[]},{"given":"Harald","family":"Ruess","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/3-540-48685-2_15","volume-title":"Rewriting Techniques and Applications","author":"L. Bachmair","year":"1999","unstructured":"Bachmair, L., Ramakrishnan, C., Ramakrishnan, I.V., Tiwari, A.: Normalization via rewrite closures. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 190\u2013204. Springer, Heidelberg (1999)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10720084_16","volume-title":"Frontiers of Combining Systems","author":"L. Bachmair","year":"2000","unstructured":"Bachmair, L., Ramakrishnan, I.V., Tiwari, A., Vigneron, L.: Congruence closure modulo associativity and commutativity. In: Kirchner, H. (ed.) FroCos 2000. LNCS(LNAI), vol.\u00a01794, pp. 245\u2013259. Springer, Heidelberg (2000)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: McAllester, D. (ed.) 17th Intl Conf on Automated Deduction (2000)","DOI":"10.1007\/10721959_5"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/3-540-58467-6_28","volume-title":"KI-94: Advances in Artificial Intelligence","author":"G. Becher","year":"1994","unstructured":"Becher, G., Petermann, U.: Rigid unification by completion and rigid paramodulation. In: Dreschler-Fischer, L., Nebel, B. (eds.) KI 1994. LNCS(LNAI), vol.\u00a0861, pp. 319\u2013330. Springer, Heidelberg (1994)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"678","DOI":"10.1007\/3-540-58156-1_49","volume-title":"Automated Deduction - CADE-12","author":"B. Beckert","year":"1994","unstructured":"Beckert, B.: A completion-based method for mixed universal and rigid E- unification. In: Bundy, A. (ed.) CADE 1994. LNCS(LNAI), vol.\u00a0814, pp. 678\u2013692. Springer, Heidelberg (1994)"},{"issue":"1-2","key":"17_CR7","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","volume":"166","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A., Voronkov, A.: The undecidability of simultaneous rigid E- unification. Theoretical Computer Science\u00a0166(1-2), 291\u2013300 (1996)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"17_CR8","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1005996623714","volume":"20","author":"A. Degtyarev","year":"1998","unstructured":"Degtyarev, A., Voronkov, A.: What you always wanted to know about rigid E-unification. Journal of Automated Reasoning\u00a020(1), 47\u201380 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(90)90061-L","volume":"87","author":"J. Gallier","year":"1990","unstructured":"Gallier, J., Narendran, P., Plaisted, D., Snyder, W.: Rigid E-unification: Np- completeness and applications to equational matings. Information and Computation\u00a087, 129\u2013195 (1990)","journal-title":"Information and Computation"},{"issue":"2","key":"17_CR10","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/128749.128754","volume":"39","author":"J. Gallier","year":"1992","unstructured":"Gallier, J., Narendran, P., Raatz, S., Snyder, W.: Theorem proving using equational matings and rigid E-unification. Journal of the Association for Computing Machinery\u00a039(2), 377\u2013429 (1992)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/BFb0022569","volume-title":"Computational Logic and Proof Theory","author":"J. Goubault","year":"1993","unstructured":"Goubault, J.: A rule-based algorithm for rigid E-unification. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol.\u00a0713, pp. 202\u2013210. Springer, Heidelberg (1993)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1997","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 23\u201337. Springer, Heidelberg (1997)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/3-540-59338-1_25","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"E. Kogel de","year":"1995","unstructured":"de Kogel, E.: Rigid E-unification simplified. In: Baumgartner, P., Posegga, J., H\u00e4hnle, R. (eds.) TABLEAUX 1995. LNCS(LNAI), vol.\u00a0918, pp. 17\u201330. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T06:40:27Z","timestamp":1553323227000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/10721959_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}