{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T15:02:08Z","timestamp":1725721328889},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642376504"},{"type":"electronic","value":"9783642376511"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37651-1_9","type":"book-chapter","created":{"date-parts":[[2013,4,5]],"date-time":"2013-04-05T04:10:01Z","timestamp":1365135001000},"page":"216-238","source":"Crossref","is-referenced-by-count":2,"title":["Narrowing Based Inductive Proof Search"],"prefix":"10.1007","author":[{"given":"Claude","family":"Kirchner","sequence":"first","affiliation":[]},{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"additional","affiliation":[]},{"given":"Fabrice","family":"Nahon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"9_CR2","volume-title":"Principles of Programming Languages (POPL 2003)","author":"G. Barthe","year":"2003","unstructured":"Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure Patterns Type Systems. In: Principles of Programming Languages (POPL 2003), ACM, New Orleans (2003)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-61464-8_73","volume-title":"Rewriting Techniques and Applications","author":"N. Berregeb","year":"1996","unstructured":"Berregeb, N., Bouhoula, A., Rusinowitch, M.: SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 428\u2013431. Springer, Heidelberg (1996)"},{"key":"9_CR4","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":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge University Press (2005)","DOI":"10.1017\/CBO9780511543326"},{"issue":"1-2","key":"9_CR6","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H. Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction=i-axiomatization+first-order consistency. Inf. Comput.\u00a0159(1-2), 151\u2013186 (2000)","journal-title":"Inf. Comput."},{"key":"9_CR7","unstructured":"Deplagne, E.: Syst\u00e8me de preuve modulo r\u00e9currence. Th\u00e8se de doctorat, Universit\u00e9 Nancy 1 (November 2002)"},{"key":"9_CR8","unstructured":"Deplagne, E., Kirchner, C.: Induction as deduction modulo. Research report A04-R-468, LORIA (November 2004)"},{"key":"9_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-540-45085-6_26","volume-title":"Automated Deduction \u2013 CADE-19","author":"E. Deplagne","year":"2003","unstructured":"Deplagne, E., Kirchner, C., Kirchner, H., Nguyen, Q.-H.: Proof Search and Proof Check for Equational and Inductive Theorems. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 297\u2013316. Springer, Heidelberg (2003)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 9, pp. 535\u2013610. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"9_CR11","unstructured":"Dowek, G.: La part du Calcul. Universit\u00e9 de Paris 7, M\u00e9moire d\u2019habilitation (1999)"},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1017\/S0960129500003236","volume":"11","author":"G. Dowek","year":"2001","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: HOL-\u03bb\u03c3 an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science\u00a011(1), 21\u201345 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"9_CR13","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning\u00a031(1), 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR14","unstructured":"Ferreira, M.: Termination of Term Rewriting: Well foundedness, Totality and Transformations. PhD thesis, Utrecht University (1995)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-56393-8_17","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1992","unstructured":"Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 226\u2013241. Springer, Heidelberg (1992); Published in 1993"},{"key":"9_CR16","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol.\u00a07. Cambridge University Press (1989)"},{"key":"9_CR17","unstructured":"Huet, G.: Constrained Resolution: A Complete Method for Higher Order Logic. PhD thesis, Case Western Reserve University (1972)"},{"key":"9_CR18","series-title":"LNCS","first-page":"318","volume-title":"Proceedings 5th International Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical Forms and Unification. In: Bibel, W., Kowalski, R. (eds.) Proceedings 5th International Conference on Automated Deduction. LNCS, vol.\u00a087, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"issue":"2","key":"9_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., Zhang, H.: An overview of rewrite rule laboratory (RRL). J. Computer and Mathematics with Applications\u00a029(2), 91\u2013114 (1995)","journal-title":"J. Computer and Mathematics with Applications"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Kirchner, C., Kirchner, H.: Rewriting, solving, proving. A preliminary version of a book (1999), \n                  \n                    http:\/\/www.loria.fr\/~ckirchne\/rsp.ps.gz","DOI":"10.1007\/978-3-642-59851-7_9"},{"issue":"3","key":"9_CR21","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue d\u2019Intelligence Artificielle\u00a04(3), 9\u201352 (1990); Special issue on Automatic Deduction","journal-title":"Revue d\u2019Intelligence Artificielle"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Musser, D.: On proving inductive properties of abstract data types. In: Proceedings, Symposium on Principles of Programming Languages, vol.\u00a07, Association for Computing Machinery (1980)","DOI":"10.1145\/567446.567461"},{"key":"9_CR23","unstructured":"Nahon, F.: Preuve par induction dans le calcul des s\u00e9quents modulo. PhD thesis, Universit\u00e9 Henri Poincar\u00e9 - Nancy I, Nancy, France, October 26 (2007)"},{"issue":"1-2","key":"9_CR24","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10472-009-9154-5","volume":"55","author":"F. Nahon","year":"2009","unstructured":"Nahon, F., Kirchner, C., Kirchner, H., Brauner, P.: Inductive Proof Search Modulo. Annals of Mathematics and Artificial Intelligence\u00a055(1-2), 123\u2013154 (2009)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9_CR25","unstructured":"Steel, G.: Proof by consistency - a literature survey (March 1999)"},{"key":"9_CR26","unstructured":"Wack, B.: Typage et d\u00e9duction dans le calcul de r\u00e9\u00e9criture. Th\u00e8se de doctorat, Universit\u00e9 Henri Poincar\u00e9 - Nancy I, October 7 (2005)"}],"container-title":["Lecture Notes in Computer Science","Programming Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37651-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T03:54:30Z","timestamp":1557633270000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37651-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642376504","9783642376511"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37651-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}