{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T09:32:36Z","timestamp":1742635956864,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584674"},{"type":"electronic","value":"9783540489795"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58467-6_28","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:13:06Z","timestamp":1330272786000},"page":"319-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Rigid unification by completion and rigid paramodulation"],"prefix":"10.1007","author":[{"given":"G\u00e9rard","family":"Becher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Petermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"issue":"2","key":"28_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, 1981.","journal-title":"J.ACM"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"G. Becher and U. Petermann. Rigid E-Unification by Completion and Rigid Paramodulation. Technical report, Cahiers du LAIAC (n. 22) Univ. of Caen, 1993.","DOI":"10.1007\/3-540-58467-6_28"},{"key":"28_CR3","unstructured":"B. Beckert. Ein vervollst\u00e4ndigungsbasiertes Verfahren zur Behandlung von Gleichheit im Tableaukalk\u00fcl mit freien Variablen. Master's thesis, Karlsruhe (TH), 1993."},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, 1st edition, 1982.","DOI":"10.1007\/978-3-322-90100-2_1"},{"key":"28_CR5","unstructured":"H. Comon. Solving inequations in term algebras. In C. S. P. IEEE, editor, Proceedings, LICS, Philadelphia, 1990."},{"issue":"1&2","key":"28_CR6","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 3(1&2):69\u2013116, February\/April 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"28_CR7","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0747-7171(92)90010-2","volume":"14","author":"D. J. Dougherty","year":"1992","unstructured":"D. J. Dougherty and P. Johann. An Improved General E-Unification Method. Journal of Symbolic Computation, 14:303\u2013320, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"28_CR8","first-page":"1","volume":"40","author":"J. Gallier","year":"1993","unstructured":"J. Gallier, P. Narendran, D. Plaisted, S. Raatz, and W. Snyder. An Algorithm for finding Canonical Sets of Ground Rewrite Rules in Polynomial Time. Journal of the A.C.M., 40:1\u201316, January 1993.","journal-title":"Journal of the A.C.M."},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-Completeness and Applications to Equational Matings. Information and Computation, pages 129\u2013195, 1990.","DOI":"10.1016\/0890-5401(90)90061-L"},{"key":"28_CR10","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J. Gallier","year":"1989","unstructured":"J. Gallier and W. Snyder. Complete Sets of Transformations for General E-Unification. Theoretical Computer Science, 67:203\u2013260, 1989.","journal-title":"Theoretical Computer Science"},{"key":"28_CR11","unstructured":"J. Goubault. A Rule-Based Algorithm for Rigid E-Unification. In 3rd Kurt G\u00f6del Colloquium '93, volume 713 of LNCS. Springer-Verlag, 1993."},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"J.-M. Hullot. Canonical Forms and Unification. In Proceedings CADE, pages 318\u2013334. Springer-Verlag, 1980. Lecture Notes in Artificial Intelligence 87.","DOI":"10.1007\/3-540-10009-1_25"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving Equations in Abstract Algebras: A Rule-based Survey of Unification. Computational Logic. Essays in Honour of Alan Robinson, pages 257\u2013321, 1991.","DOI":"10.1016\/0743-1066(92)90027-Z"},{"key":"28_CR14","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1147\/rd.254.0327","volume":"4","author":"D. Kozen","year":"1981","unstructured":"D. Kozen. Positive first-order logic is NP-complete. IBM Journal of Research and Development, 4:327\u2013332, 1981.","journal-title":"IBM Journal of Research and Development"},{"key":"28_CR15","first-page":"210","volume":"95","author":"J. Kruskal","year":"1960","unstructured":"J. Kruskal. Well Quasi Ordering, the Tree Problem and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210\u2013225, 1960.","journal-title":"Transactions of the American Mathematical Society"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"D. W. Loveland. Mechanical Theorem Proving by Model Elimination. JACM, 15(2), 1978.","DOI":"10.1145\/321450.321456"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"G. Nelson and D. C. Oppen. Fast Decision Procedures Based on Congruence Closure. Journal of Association for Computer Machinery, 27(2), April 1980.","DOI":"10.1145\/322186.322198"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"D. A. Plaisted. A simple non-termination test for the Knuth-Bendix method. In Proc 8th CADE, LNCS 230, pages 79\u201388. Springer, 1986.","DOI":"10.1007\/3-540-16780-3_81"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"D. A. Plaisted. Polynomial Time Termination and Constraint Satisfaction Tests. In Rewriting Techniques and Applications, pages 405\u2013420, Montreal, June 1993.","DOI":"10.1007\/3-540-56868-9_30"}],"container-title":["Lecture Notes in Computer Science","KI-94: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58467-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:30:41Z","timestamp":1742596241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58467-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584674","9783540489795"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-58467-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"3 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}