{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T12:30:43Z","timestamp":1648989043169},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2010,4,1]],"date-time":"2010-04-01T00:00:00Z","timestamp":1270080000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2010,4]]},"DOI":"10.1007\/s10472-010-9200-3","type":"journal-article","created":{"date-parts":[[2010,6,28]],"date-time":"2010-06-28T02:21:25Z","timestamp":1277691685000},"page":"155-183","source":"Crossref","is-referenced-by-count":0,"title":["Simplified handling of iterated term schemata"],"prefix":"10.1007","volume":"58","author":[{"given":"Vincent","family":"Aravantinos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ricardo","family":"Caferra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,6,29]]},"reference":[{"key":"9200_CR1","unstructured":"Amaniss, A., Hermann, M., Lugiez, D.: Etude comparative des m\u00e9thodes de sch\u00e9matisation de s\u00e9quences infinies de termes du premier ordre. Research Report 93-R-114, Centre de Recherche en Informatique de Nancy (1993)"},{"key":"9200_CR2","unstructured":"Aravantinos, V.: Sch\u00e9mas de preuves et de formules: vers plus de structure et d\u2019efficacit\u00e9 en d\u00e9duction automatique. Master thesis, Institut National Polytechnique de Grenoble & Universit\u00e9 Joseph Fourier (2007). http:\/\/membres-lig.imag.fr\/aravantinos"},{"key":"9200_CR3","doi-asserted-by":"crossref","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: A schemata calculus for propositional logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX. Lecture Notes in Computer Science, vol. 5607, pp. 32\u201346. Springer (2009)","DOI":"10.1007\/978-3-642-02716-1_4"},{"key":"9200_CR4","doi-asserted-by":"crossref","unstructured":"Bensaid, H., Caferra, R., Peltier, N.: Dei: a theorem prover for terms with integer exponents. In: Schmidt, R.A. (ed.) CADE. Lecture Notes in Computer Science, vol. 5663, pp. 146\u2013150. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_11"},{"key":"9200_CR5","doi-asserted-by":"crossref","unstructured":"Bensaid, H., Caferra, R., Peltier, N.: Perfect discrimination graphs: indexing terms with integer exponents. In: Giesl, J., H\u00e4hnle, R. (eds.) International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science. Springer (2010, to appear)","DOI":"10.1007\/978-3-642-14203-1_32"},{"key":"9200_CR6","doi-asserted-by":"crossref","unstructured":"Chen, H., Hsiang, J., Kong, H.: On finite representations of infinite sequences of terms. In: Conditional and Typed Rewriting Systems. LNCS 516, pp. 100\u2013114. Springer (1990)","DOI":"10.1007\/3-540-54317-1_83"},{"key":"9200_CR7","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BF01294596","volume":"28","author":"H Comon","year":"1995","unstructured":"Comon, H.: On unification of terms with integer exponents. Math. Syst. Theory 28, 67\u201388 (1995)","journal-title":"Math. Syst. Theory"},{"key":"9200_CR8","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata (2005). Release 12 October 2007"},{"key":"9200_CR9","unstructured":"Hermann, M.: Divergence des syst\u00e8mes de r\u00e9\u00e9criture et sch\u00e9matisation des ensembles infinis de termes. Habilitation, Universit\u00e9 Henri Poincar\u00e9 Nancy 1 (1994)"},{"key":"9200_CR10","unstructured":"Hermann, M.: Overview of existing recurrent schematizations. In: Proc. of the CADE-13 Workshop on Term Schematization and their Applications (1996)"},{"issue":"1\u20132","key":"9200_CR11","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/S0304-3975(96)00052-7","volume":"176","author":"M Hermann","year":"1997","unstructured":"Hermann, M., Galbav\u00fd, R.: Unification of infinite sets of terms schematized by primal grammars. Theor. Comp. Sci. 176(1\u20132), 111\u2013158 (1997)","journal-title":"Theor. Comp. Sci."},{"key":"9200_CR12","doi-asserted-by":"crossref","unstructured":"Peltier, N.: The first order theory of primal grammars is decidable. Theor. Comp. Sci. 323, 267\u2013320","DOI":"10.1016\/j.tcs.2004.04.007"},{"key":"9200_CR13","doi-asserted-by":"crossref","unstructured":"Salzer, G.: The unification of infinite sets of terms and its applications. In: Logic Programming and Automated Reasoning (LPAR\u201992). LNAI 624, pp. 409\u2013429. Springer (1992)","DOI":"10.1007\/BFb0013079"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-010-9200-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-010-9200-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-010-9200-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T09:43:16Z","timestamp":1559209396000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-010-9200-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4]]},"references-count":13,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["9200"],"URL":"https:\/\/doi.org\/10.1007\/s10472-010-9200-3","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4]]}}}