{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:27:01Z","timestamp":1759638421005},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642408847"},{"type":"electronic","value":"9783642408854"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40885-4_2","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T11:20:19Z","timestamp":1378898419000},"page":"7-22","source":"Crossref","is-referenced-by-count":11,"title":["Combining Superposition and Induction: A Practical Realization"],"prefix":"10.1007","author":[{"given":"Abdelkader","family":"Kersani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E. Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 84\u201399. Springer, Heidelberg (2009)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Aravantinos, V., Echenim, M., Peltier, N.: A resolution calculus for first-order schemata. Fundamenta Informaticae (accepted for publication, to appear, 2013)","DOI":"10.3233\/FI-2013-855"},{"issue":"3-4","key":"2_CR3","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/j.jsc.2003.10.005","volume":"41","author":"M. Baaz","year":"2006","unstructured":"Baaz, M., Leitsch, A.: Towards a clausal analysis of cut-elimination. J. Symb. Comput.\u00a041(3-4), 381\u2013410 (2006)","journal-title":"J. Symb. Comput."},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierachic first-order theories. Appl. Algebra Eng. Commun. Comput.\u00a05, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44881-0_24","volume-title":"Rewriting Techniques and Applications","author":"G. Barthe","year":"2003","unstructured":"Barthe, G., Stratulat, S.: Validation of the javacard platform with implicit induction techniques. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 337\u2013351. Springer, Heidelberg (2003)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-22438-6_9","volume-title":"Automated Deduction \u2013 CADE-23","author":"P. Baumgartner","year":"2011","unstructured":"Baumgartner, P., Tinelli, C.: Model Evolution with Equality Modulo Built-in Theories. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 85\u2013100. Springer, Heidelberg (2011)"},{"key":"2_CR7","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":"2_CR8","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":"2_CR9","unstructured":"Dunchev, T.: Automation of cut-elimination in proof schemata. PhD thesis, T.U. Vienna (2012)"},{"key":"2_CR10","unstructured":"Dunchev, T., Leitsch, A., Rukhaia, M., Weller, D.: Ceres for first-order schemata, Research Report (2013), http:\/\/arxiv.org\/abs\/1303.4257"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-31365-3_20","volume-title":"Automated Reasoning","author":"S. Falke","year":"2012","unstructured":"Falke, S., Kapur, D.: Rewriting induction + linear arithmetic = decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 241\u2013255. Springer, Heidelberg (2012)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"2_CR13","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., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 469\u2013484. Springer, Heidelberg (2001)"},{"key":"2_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-45085-6_3","volume-title":"Automated Deduction \u2013 CADE-19","author":"J. Giesl","year":"2003","unstructured":"Giesl, J., Kapur, D.: Deciding inductive validity of equations. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 17\u201331. Springer, Heidelberg (2003)"},{"issue":"4","key":"2_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1805950.1805957","volume":"11","author":"M. Horbach","year":"2010","unstructured":"Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Trans. Comput. Logic\u00a011(4), 1\u201335 (2010)","journal-title":"ACM Trans. Comput. Logic"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-38574-2_4","volume-title":"Automated Deduction \u2013 CADE-24","author":"A. Kersani","year":"2013","unstructured":"Kersani, A., Peltier, N.: Completeness and Decidability Results for First-Order Clauses with Indices. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 58\u201375. Springer, Heidelberg (2013)"},{"key":"2_CR17","unstructured":"McCune, W.: Prover9 and mace4 (2005\u20132010), http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"key":"2_CR18","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. North-Holland (2001)"},{"key":"2_CR19","unstructured":"Rukhaia, M.: CERES in Proof Schemata. PhD thesis, T.U. Vienna (2012)"},{"key":"2_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/11554554_20","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Stratulat","year":"2005","unstructured":"Stratulat, S.: Automatic \u2018Descente infinie\u2019 induction reasoning. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 262\u2013276. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40885-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T20:18:47Z","timestamp":1596485927000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40885-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642408847","9783642408854"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40885-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}