{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:22Z","timestamp":1749125182091},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_99","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:50:45Z","timestamp":1330293045000},"page":"343-357","source":"Crossref","is-referenced-by-count":2,"title":["Unification in pseudo-linear sort theories is decidable"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"36_CR1","doi-asserted-by":"crossref","unstructured":"Bruno Bogaert and Sophie Tison. Equality and disequality constraints on direct subterms in tree automata. In A. Finkel and M. Jantzen, editors, Proc. of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92, volume 577 of LNCS, pages 161\u2013171. Springer, 1992.","DOI":"10.1007\/3-540-55210-3_181"},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"Anne-C\u00e9cile Caron, Hubert Comon, Jean-Luc Coquid\u00e9, Max Dauchet, and Florent Jacquemard. Pumping, cleaning and symbolic constraints solving. In Serge Abiteboul and Eli Shamir, editors, Automata Languages and Programming. 21st International Colloquium, ICALP'94, volume 820 of LNCS, pages 436\u2013447. Springer, 1994.","DOI":"10.1007\/3-540-58201-0_88"},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Hubert Comon. Inductive proofs by specification transformations. In Rewriting Techniques and Applications, RTA-89, volume 355 of LNCS, pages 76\u201391. Springer, 1989.","DOI":"10.1007\/3-540-51081-8_101"},{"key":"36_CR4","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, chapter 6, pages 243\u2013320. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"36_CR5","doi-asserted-by":"crossref","unstructured":"Alan M. Frisch and Anthony G. Cohn. An abstract view of sorted unification. In 11th International Conference on Automated Deduction, CADE-11, LNCS 607, volume 607 of LNCS, pages 178\u2013192. Springer, 1992.","DOI":"10.1007\/3-540-55602-8_164"},{"key":"36_CR6","unstructured":"Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J.L. Lassez and G. Plotkin, editors, Computational Logic, Essays in Honor of Alan Robinson, chapter 8, pages 257\u2013321. MIT Press, 1991."},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Manfred Schmidt-Schau\u00df. Computational aspects of an order sorted logic with term declarations, volume 395 of LNAI. Springer, 1989.","DOI":"10.1007\/BFb0024065"},{"key":"36_CR8","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J. Siekmann","year":"1989","unstructured":"J\u00f6rg Siekmann. Unification theory. Journal of Symbolic Computation, Special Issue on Unification, 7:207\u2013274, 1989.","journal-title":"Journal of Symbolic Computation, Special Issue on Unification"},{"key":"36_CR9","doi-asserted-by":"crossref","unstructured":"Tom\u00e1s E. Uribe. Sorted unification using set constraints. In 11th International Conference on Automated Deduction, CADE-11, volume 607 of LNCS, pages 163\u2013177. Springer, 1992.","DOI":"10.1007\/3-540-55602-8_163"},{"key":"36_CR10","unstructured":"Christoph Walther. Unification in many-sorted theories. In Proceedings of the 6th ECAI, pages 383\u2013392. North-Holland, 1983."},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"Christoph Weidenbach. Unification in sort theories and its applications. Annals of Mathematics and Artificial Intelligence. To appear.","DOI":"10.1007\/BF02127750"},{"key":"36_CR12","unstructured":"Christoph Weidenbach. Extending the resolution method with sorts. In Proc. of 13th International Joint Conference on Artificial Intelligence, IJCAI-93, pages 60\u201365. Morgan Kaufmann, 1993."},{"issue":"6","key":"36_CR13","first-page":"887","volume":"3","author":"C. Weidenbach","year":"1995","unstructured":"Christoph Weidenbach. First-order tableaux with sorts. Journal of the Interest Group in Pure and Applied Logics, IGPL, 3(6):887\u2013906, 1995.","journal-title":"Journal of the Interest Group in Pure and Applied Logics, IGPL"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_99.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:28Z","timestamp":1605647248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_99"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_99","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}