{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T23:24:00Z","timestamp":1743031440070,"version":"3.40.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319155784"},{"type":"electronic","value":"9783319155791"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15579-1_20","type":"book-chapter","created":{"date-parts":[[2015,2,23]],"date-time":"2015-02-23T08:36:13Z","timestamp":1424680573000},"page":"263-274","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning on Schemas of Formulas: An Automata-Based Approach"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Peltier","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,2,24]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-13089-2_5","volume-title":"Language and Automata Theory and Applications","author":"V Aravantinos","year":"2010","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: Complexity of the satisfiability problem for a class of propositional schemata. In: Dediu, A.-H., Fernau, H., Mart\u00edn-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 58\u201369. Springer, Heidelberg (2010)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-14203-1_26","volume-title":"Automated Reasoning","author":"V Aravantinos","year":"2010","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: RegSTAB: A SAT solver for propositional schemata. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 309\u2013315. Springer, Heidelberg (2010)"},{"key":"20_CR3","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1613\/jair.3351","volume":"40","author":"V Aravantinos","year":"2011","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: Decidability and undecidability results for propositional schemata. Journal of Artificial Intelligence Research 40, 599\u2013656 (2011)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-642-22119-4_5","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"V Aravantinos","year":"2011","unstructured":"Aravantinos, V., Peltier, N.: Schemata of SMT-problems. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 27\u201342. Springer, Heidelberg (2011)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"20_CR6","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). http:\/\/www.SMT-LIB.org"},{"key":"20_CR7","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997). http:\/\/www.grappa.univ-lille3.fr\/tata"},{"key":"20_CR8","first-page":"243","volume-title":"Formal Models and Semantics","author":"Nachum DERSHOWITZ","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.: Rewrite systems. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 243\u2013320 (1990)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 3, vol. I, pp. 100\u2013178. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"20_CR11","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. North-Holland (2001)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Wielemakers, J.: SWI-Prolog version 7 extensions. In: WLPE 2014, July 2014","DOI":"10.1515\/transcript.9783839430095.intro"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15579-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,21]],"date-time":"2023-01-21T05:43:01Z","timestamp":1674279781000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15579-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319155784","9783319155791"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15579-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"24 February 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}