{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:32:56Z","timestamp":1725485576711},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_19","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T22:48:36Z","timestamp":1180651716000},"page":"278-291","source":"Crossref","is-referenced-by-count":15,"title":["Theorem Proving with Sequence Variables and Flexible Arity Symbols"],"prefix":"10.1007","author":[{"given":"Temur","family":"Kutsia","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"19_CR1","unstructured":"B. Buchberger, C. Dupr\u00e9, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, and W. Windsteiger. The Theorema project: A progress report. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000), pages 98\u2013113, St.Andrews, UK, 6\u20137 August 2000."},{"key":"19_CR2","unstructured":"L. Bachmair, N. Dershowitz, and D. Plaisted. Completion without failure. In H. A\u00eft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2, pages 1\u201330. Elsevier Science, 1989."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In M. E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence, pages 427\u2013441, Kaiserslautern, Germany, July 1990. Springer Verlag.","DOI":"10.1007\/3-540-52885-7_105"},{"issue":"3","key":"19_CR4","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217\u2013247, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"19_CR5","unstructured":"B. Buchberger and M. Marin. Proving by simplification. In Proceedings of the First International Theorema Workshop, RISC-Linz Technical Report 97-20, Hagenberg, Austria, 9\u201310 June 1997."},{"key":"19_CR6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That.","author":"F. Baader","year":"1998","unstructured":"F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, New York, 1998."},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"F. Baader and W. Snyder. Unification theory. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 8, pages 445\u2013532. Elsevier Science, 2001.","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"19_CR8","first-page":"1","volume-title":"Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming","author":"B. Buchberger","year":"1996","unstructured":"B. Buchberger. Mathematica as a rewrite language. In T. Ida, A. Ohori, and M. Takeichi, editors, Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming, pages 1\u201313, Shonan Village Center, Japan, 1\u20134 November 1996. World Scientific."},{"key":"19_CR9","unstructured":"B. Buchberger. Personal communication, 2001."},{"issue":"3","key":"19_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279\u2013301, 1982.","journal-title":"Theoretical Computer Science"},{"key":"19_CR11","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewriting systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 243\u2013320. Elsevier Science, Amsterdam, 1990."},{"key":"19_CR12","volume-title":"Technical report","author":"M. R. Genesereth","year":"1995","unstructured":"M. R. Genesereth. Epilog for Lisp 2.0 Manual. Technical report, Epistemics Inc., Palo Alto, California, US, 1995."},{"key":"19_CR13","volume-title":"Technical Report Logic-92-1","author":"M. R. Genesereth","year":"1992","unstructured":"M. R. Genesereth and R. E. Fikes. Knowledge Interchange Format, Version 3.0 Reference Manual. Technical Report Logic-92-1, Computer Science Department, Stanford University, Stanford, California, US, June 1992."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"S. Ginsburg and X. S. Wang. Pattern matching by Rs-operations: Toward a unified approach to querying sequenced data. In Proceedings of the 11th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 293\u2013300, San Diego, California, US, 2\u20134 June 1992.","DOI":"10.1145\/137097.137895"},{"key":"19_CR15","unstructured":"M. Hamana. Term rewriting with sequences. In Proceedings of the First International Theorema Workshop, RISC-Linz Technical Report 97-20, Hagenberg, Austria, 9\u201310 June 1997."},{"key":"19_CR16","unstructured":"P. Hayes and C. Menzel. Semantics of knowledge interchange format. \n http:\/\/reliant.teknowledge.com\/IJCAI01\/HayesMenzel-SKIF-IJCAI2001.pdf\n \n , 2001."},{"key":"19_CR17","volume-title":"Two generalizations of the recursive path ordering","author":"S. Kamin","year":"1980","unstructured":"S. Kamin and J.-J. L\u00e9vy. Two generalizations of the recursive path ordering. Unpublished note, Department of Computer Science, University of Illinois, Urbana, Illinois, US, 1980."},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"T. Kutsia. Pattern unification with sequence variables and flexible arity symbols. In M. Ojeda-Asiego, editor, Proceedings of the Workshop on Unification in Non-Classical Logics, volume 66, issue 5 of Electronic Notes on Theoretical Computer Science. Elsevier Science, 2002.","DOI":"10.1016\/S1571-0661(04)80514-0"},{"key":"19_CR19","volume-title":"SFB Report 02-6","author":"T. Kutsia","year":"2002","unstructured":"T. Kutsia. Unification in a free theory with sequence variables and flexible arity symbols and its extensions. SFB Report 02-6, Johannes Kepler University, Linz, Austria, 2002."},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"T. Kutsia. Unification with sequence variables and flexible arity symbols and its extension with pattern-terms. In Artificial Intelligence, Automated Reasoning and Symbolic Computation. Proceedings of Joint AICS\u20192002-Calculemus\u20192002 conference, volume 2385 of Lecture Notes in Artificial Intelligence, Marseille, France, 1\u20135 July 2002. Springer Verlag.","DOI":"10.1007\/3-540-45470-5_26"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"G. Mecca and A. J. Bonner. Sequences, Datalog and transducers. In Proceedings of the Fourteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 23\u201335, San Jose, California, US, 22\u201325 May 1995.","DOI":"10.1145\/212433.212440"},{"key":"19_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the European Symposium of Programming","author":"R. Nieuwenhuis","year":"1992","unstructured":"R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In B. Krieg-Br\u00fcckner, editor, Proceedings of the European Symposium of Programming, volume 582 of Lecture Notes in Computer Science, Rennes, France, 1992. Springer Verlag."},{"key":"19_CR23","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"R. Nieuwenhuis and A. Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computation, 19:321\u2013351, 1995.","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 7, pages 371\u2013443. Elsevier Science, 2001.","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"19_CR25","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Conference of European Association for Computer Science Logic","author":"A. Rubio","year":"1995","unstructured":"A. Rubio. Theorem proving modulo associativity. In Proceedings of the Conference of European Association for Computer Science Logic, Lecture Notes in Computer Science, Paderborn, Germany, 1995. Springer Verlag."},{"key":"19_CR26","volume-title":"Technical Report No. 280","author":"M. Widera","year":"2001","unstructured":"M. Widera and C. Beierle. A term rewriting scheme for function symbols with variable arity. Technical Report No. 280, Praktische Informatik VIII, FernUniversit\u00e4t Hagen, Germany, 2001."},{"key":"19_CR27","unstructured":"S. Wolfram. The Mathematica Book. Cambridge University Press and Wolfram Research, Inc., fourth edition, 1999."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T20:45:29Z","timestamp":1550349929000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}