{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:53:56Z","timestamp":1725515636401},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_21","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T09:00:57Z","timestamp":1340614857000},"page":"310-325","source":"Crossref","is-referenced-by-count":1,"title":["Reasoning on Schemata of Formul\u00e6"],"prefix":"10.1007","author":[{"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P. Aczel","year":"1977","unstructured":"Aczel, P.: An Introduction to Inductive Definitions. In: Barwise, K.J. (ed.) Handbook of Mathematical Logic, pp. 739\u2013782. North-Holland, Amsterdam (1977)"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02716-1_4","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"V. Aravantinos","year":"2009","unstructured":"Aravantinos, V., Caferra, R., Peltier, N.: A Schemata Calculus for Propositional Logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol.\u00a05607, pp. 32\u201346. Springer, Heidelberg (2009)"},{"key":"21_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\u00a040, 599\u2013656 (2011)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"21_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.\u00a06793, pp. 27\u201342. Springer, Heidelberg (2011)"},{"issue":"2-3","key":"21_CR5","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/j.tcs.2008.02.043","volume":"403","author":"M. Baaz","year":"2008","unstructured":"Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: CERES: An analysis of F\u00fcrstenberg\u2019s proof of the infinity of primes. Theor. Comput. Sci.\u00a0403(2-3), 160\u2013175 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-14203-1_24","volume-title":"Automated Reasoning","author":"D. Baelde","year":"2010","unstructured":"Baelde, D., Miller, D., Snow, Z.: Focused Inductive Theorem Proving. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 278\u2013292. Springer, Heidelberg (2010)"},{"key":"21_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/BFb0013087","volume-title":"Logic Programming and Automated Reasoning","author":"A. Bouhoula","year":"1992","unstructured":"Bouhoula, A., Kounalis, E., Rusinowitch, M.: SPIKE, an Automatic Theorem Prover. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 460\u2013462. Springer, Heidelberg (1992)"},{"key":"21_CR9","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/BF00881856","volume":"14","author":"A. Bouhoula","year":"1995","unstructured":"Bouhoula, A., Rusinowitch, M.: Implicit induction in conditional theories. Journal of Automated Reasoning\u00a014, 14\u2013189 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-52885-7_75","volume-title":"10th International Conference on Automated Deduction","author":"R.S. Boyer","year":"1990","unstructured":"Boyer, R.S., Moore, J.S.: A Theorem Prover for a Computational Logic. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 1\u201315. Springer, Heidelberg (1990)"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 845\u2013911. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 14, pp. 913\u2013962. North-Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50016-3"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Echenim, M., Peltier, N.: Reasoning on Schemata of Formulae. Technical report, CoRR, abs\/1204.2990 (2012)","DOI":"10.1007\/978-3-642-31374-5_21"},{"key":"21_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45744-5_41","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Kapur, D.: Decidable Classes of Inductive Theorems. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 469\u2013484. Springer, Heidelberg (2001)"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/3-540-56922-7_3","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"1993","unstructured":"Gupta, A., Fisher, A.L.: Parametric Circuit Representation Using Inductive Boolean Functions. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 15\u201328. Springer, Heidelberg (1993)"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Kapur, D., Musser, D.: Proof by consistency. Artificial Intelligence\u00a031 (1987)","DOI":"10.1016\/0004-3702(87)90017-8"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/3-540-44693-1_41","volume-title":"STACS 2001","author":"G. Lenzi","year":"2001","unstructured":"Lenzi, G.: A New Logical Characterization of B\u00fcchi Automata. In: Ferreira, A., Reichel, H. (eds.) STACS 2001. LNCS, vol.\u00a02010, pp. 467\u2013477. Springer, Heidelberg (2001)"},{"key":"21_CR18","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"D.M. Park","year":"1976","unstructured":"Park, D.M.: Finiteness is Mu-ineffable. Theoretical Computer Science\u00a03, 173\u2013181 (1976)","journal-title":"Theoretical Computer Science"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive Definitions in the system Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 328\u2013345. Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31374-5_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T09:37:36Z","timestamp":1556876256000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}