{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:54Z","timestamp":1761611274043},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540232124"},{"type":"electronic","value":"9783540302100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30210-0_14","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T05:34:36Z","timestamp":1295328876000},"page":"157-170","source":"Crossref","is-referenced-by-count":8,"title":["Solving Equations Involving Sequence Variables and Sequence Functions"],"prefix":"10.1007","author":[{"given":"Temur","family":"Kutsia","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"5","key":"14_CR1","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1016\/S0747-7171(89)80056-2","volume":"8","author":"H. Abdulrab","year":"1990","unstructured":"Abdulrab, H., P\u00e9cuchet, J.-P.: Solving word equations. J. Symbolic Computation\u00a08(5), 499\u2013522 (1990)","journal-title":"J. Symbolic Computation"},{"issue":"2","key":"14_CR2","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. J. Symbolic Computation\u00a021(2), 211\u2013244 (1996)","journal-title":"J. Symbolic Computation"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","volume-title":"Handbook of Automated Reasoning","author":"F. Baader","year":"2001","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 8, pp. 445\u2013532. Elsevier Science, Amsterdam (2001)"},{"issue":"3","key":"14_CR4","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BF00881869","volume":"11","author":"W.W. Bledsoe","year":"1993","unstructured":"Bledsoe, W.W., Feng, G.: Set-Var. J. Automated Reasoning\u00a011(3), 293\u2013314 (1993)","journal-title":"J. Automated Reasoning"},{"key":"14_CR5","series-title":"LNAI","volume-title":"A Tight, Practical Integration of Relations and Functions","year":"1999","unstructured":"Boley, H. (ed.): A Tight, Practical Integration of Relations and Functions. LNCS (LNAI), vol.\u00a01712. Springer, Heidelberg (1999)"},{"key":"14_CR6","unstructured":"Buchberger, B., Dupr\u00e9, C., Jebelean, T., Kriftner, F., Nakagawa, K., Vasaru, D., Windsteiger, W.: The Theorema project: A progress report. In: Kerber, M., Kohlhase, M. (eds.) Proc. of Calculemus 2000 Conference, St. Andrews, UK, August 6-7, pp. 98\u2013113 (2000)"},{"key":"14_CR7","unstructured":"Ginsberg, M.L.: User\u2019s guide to the MVL system. Technical report, Stanford University, Stanford, California, US (1989)"},{"issue":"1","key":"14_CR8","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/78935.78938","volume":"37","author":"J. Jaffar","year":"1990","unstructured":"Jaffar, J.: Minimal and complete word unification. J. ACM\u00a037(1), 47\u201385 (1990)","journal-title":"J. ACM"},{"key":"14_CR9","unstructured":"Kohlhase, M.: A mechanization of sorted higher-order logic based on the resolution principle. PhD Thesis. Universit\u00e4t des Saarlandes. Saarbr\u00fccken, Germany (1994)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Kutsia, T.: Solving and proving in equational theories with sequence variables and flexible arity symbols. Technical Report 02-31, RISC-Linz, Austria (2002)","DOI":"10.1007\/3-540-36078-6_19"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/3-540-44881-0_26","volume-title":"Rewriting Techniques and Applications","author":"T. Kutsia","year":"2003","unstructured":"Kutsia, T.: Equational prover of Theorema. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 367\u2013379. Springer, Heidelberg (2003)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Kutsia, T.: Solving equations involving sequence variables and sequence functions. Technical Report 04-01, RISC, Johannes Kepler University, Linz, Austria (2004), http:\/\/www.risc.uni-linz.ac.at\/people\/tkutsia\/papers\/SeqUnif.ps","DOI":"10.1007\/978-3-540-30210-0_14"},{"key":"14_CR13","unstructured":"Marin, M., Kutsia, T.: On the implementation of a rule-based programming system and some of its applications. In: Konev, B., Schmidt, R. (eds.) Proc. of the 4th Int. Workshop on the Implementation of Logics (WIL 2003), Almaty, Kazakhstan, pp. 55\u201368 (2003)"},{"key":"14_CR14","first-page":"361","volume-title":"Logic and Computer Science","author":"L. Paulson","year":"1990","unstructured":"Paulson, L.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361\u2013386. Academic Press, London (1990)"},{"key":"14_CR15","unstructured":"Plotkin, G.: Building in equational theories. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a07, pp. 73\u201390. Edinburgh University Press (1972)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-49674-2_14","volume-title":"Logic Program Synthesis and Transformation","author":"J. Richardson","year":"1998","unstructured":"Richardson, J., Fuchs, N.E.: Development of correct transformation schemata for Prolog programs. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol.\u00a01463, pp. 263\u2013281. Springer, Heidelberg (1998)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/BFb0052364","volume-title":"Rewriting Techniques and Applications","author":"R. Schmidt","year":"1998","unstructured":"Schmidt, R.: E-Unification for subsystems of S4. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol.\u00a01379, pp. 106\u2013120. Springer, Heidelberg (1998)"},{"key":"14_CR18","unstructured":"Wolfram, S.: The Mathematica Book, 4th edn. Cambridge University Press and Wolfram Research, Inc. (1999)"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30210-0_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:49:26Z","timestamp":1605743366000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30210-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232124","9783540302100"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30210-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}