{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:10:49Z","timestamp":1761621049770,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_26","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"297-316","source":"Crossref","is-referenced-by-count":6,"title":["Proof Search and Proof Check for Equational and Inductive Theorems"],"prefix":"10.1007","author":[{"given":"Eric","family":"Deplagne","sequence":"first","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]},{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"additional","affiliation":[]},{"given":"Quang Huy","family":"Nguyen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","volume-title":"Automated - A Basis for Applications","author":"W. Ahrendt","year":"1998","unstructured":"Ahrendt, W., Beckert, B., H\u00e4hnle, R., Menzel, W., Reil, W., Schellhorn, G., Schmitt, P.: Integrating automated and interactive theorem proving. In: Bibel, W., Schmitt, P. (eds.) Automated - A Basis for Applications, vol.\u00a01. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. In: ACM (ed.) Conf. Rec. 17th Symp. POPL, pp. 31\u201346 (1990)","DOI":"10.1145\/96709.96712"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: Proc. of 27th POPL, pp. 243\u2013253 (January 2000)","DOI":"10.1145\/325694.325727"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Proc. 16th LICS, pp. 247\u2013258 (June 2001)","DOI":"10.1109\/LICS.2001.932501"},{"issue":"3","key":"26_CR5","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. Journal of Automated Reasoning\u00a028(3), 321\u2013336 (2002)","journal-title":"Journal of Automated Reasoning"},{"issue":"3-4","key":"26_CR6","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. Journal of Automated Reasoning\u00a029(3-4), 253\u2013275 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR7","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0304-3975(01)00358-9","volume":"285","author":"P. Borovansky","year":"2002","unstructured":"Borovansky, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science\u00a0(285), 155\u2013185 (2002)","journal-title":"Theoretical Computer Science"},{"key":"26_CR8","series-title":"Lecture Notes in Artificial Intelligence","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 (LNAI), vol.\u00a0624, pp. 460\u2013462. Springer, Heidelberg (1992)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/BFb0055131","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Boulton","year":"1998","unstructured":"Boulton, R., Slind, K., Bundy, A., Gordon, M.: An interface between clam and HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 87\u2013104. Springer, Heidelberg (1998)"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation\u00a076 (1988)","DOI":"10.1016\/0890-5401(88)90005-3"},{"issue":"2","key":"26_CR12","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"Curien, P.-L., Hardin, T., L\u00e9vy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM\u00a043(2), 362\u2013397 (1996)","journal-title":"Journal of the ACM"},{"key":"26_CR13","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"26_CR14","unstructured":"Cirstea, H.: Calcul de r\u00e9\u00e9criture: fondements et applications. Th\u00e8se de Doctorat d\u2019Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9 - Nancy 1 (October 2000)"},{"issue":"3","key":"26_CR15","first-page":"427","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus \u2014 Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics\u00a09(3), 427\u2013498 (2001)","journal-title":"Logic Journal of the Interest Group in Pure and Applied Logics"},{"key":"26_CR16","unstructured":"Deplagne, E.: Syst\u00e8me de preuve modulo r\u00e9currence. Th\u00e8se de doctorat, Universit\u00e9 Nancy 1 (November 2002)"},{"issue":"1","key":"26_CR17","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"},{"key":"26_CR18","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning (2003) (to appear), See also ftp:\/\/ftp.inria.fr\/INRIA\/publication\/RR\/RR-3400.ps.gz"},{"key":"26_CR19","unstructured":"Deplagne, E., Kirchner, C.: Induction as deduction modulo. Research report, Loria (2003) (in preparation)"},{"key":"26_CR20","unstructured":"Dowek, G.: La part du Calcul. M\u00e9moire d\u2019habilitation, Universit\u00e9 de Paris 7 (1999)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/3-540-44802-0_34","volume-title":"Computer Science Logic","author":"J. Goubault-Larrecq","year":"2001","unstructured":"Goubault-Larrecq, J.: Well-founded recursive relations. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 484\u2013497. Springer, Heidelberg (2001)"},{"key":"26_CR22","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, UK (1995), Available at http:\/\/www.cl.cam.ac.uk\/users\/jrh\/papers\/reflect.dvi.gz+"},{"key":"26_CR23","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A sceptic\u2019s approach to combining hoal and mapple. Journal of Automated Reasoning\u00a021, 279\u2013294 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013321. Springer, Heidelberg (1999)"},{"issue":"4","key":"26_CR25","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal of Computing\u00a015(4), 1155\u20131194 (1986)","journal-title":"SIAM Journal of Computing"},{"key":"26_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-57826-9_135","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J. Joyce","year":"1994","unstructured":"Joyce, J., Seger, C.: The HOL-Voss system: Model-checking inside a general-purpose theorem-prover. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol.\u00a0780, pp. 185\u2013198. Springer, Heidelberg (1994)"},{"issue":"2","key":"26_CR27","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1017\/S0956796800003907","volume":"11","author":"H. Kirchner","year":"2001","unstructured":"Kirchner, H., Moreau, P.-E.: Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associativecommutative theories. Journal of Functional Programming\u00a011(2), 207\u2013251 (2001); Report LORIA A01-R-007","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"26_CR28","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":"26_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/BFb0014061","volume-title":"Typed Lambda Calculi and Applications","author":"F. Leclerc","year":"1995","unstructured":"Leclerc, F.: Termination proof of term rewriting systems with the multiset path ordering: A complete development in the system coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 312\u2013327. Springer, Heidelberg (1995)"},{"key":"26_CR30","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Proc. of 24th POPL, pp. 106\u2013119 (January 1997)","DOI":"10.1145\/263699.263712"},{"key":"26_CR31","unstructured":"Nguyen, Q.-H.: Calcul de r\u00e9\u00e9criture et automatisation du raisonnement dans les assistants de preuve. Th\u00e8se de Doctorat d\u2019Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9 - Nancy 1 (October 2002)"},{"key":"26_CR32","unstructured":"Nguyen, Q.-H.: A constructive decision procedure for equalities modulo AC. In: Ringeissen, C., Tinelli, C., Treinen, R., Verma, R. (eds.) Proc. of 18th UNIF, pp. 59\u201363 (2002)"},{"issue":"3-4","key":"26_CR33","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1023\/A:1021975117537","volume":"29","author":"Q.-H. Nguyen","year":"2002","unstructured":"Nguyen, Q.-H., Kirchner, C., Kirchner, H.: External rewriting for skeptical proof assistants. Journal of Automated Reasoning\u00a029(3-4), 309\u2013336 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"26_CR34","doi-asserted-by":"crossref","unstructured":"Necula, G., Lee, P.: Efficient representation and validation of logical proofs. In: Proc. LICS 1998, pp. 93\u2013104 (June 1998)","DOI":"10.1109\/LICS.1998.705646"},{"issue":"3","key":"26_CR35","first-page":"73","volume":"5","author":"L. Paulson","year":"1999","unstructured":"Paulson, L.: A Generic Tableau Prover and its Integration with Isabelle. Journal of Universal Computer Science\u00a05(3), 73\u201387 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"26_CR36","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)"},{"key":"26_CR37","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"Peterson, G., Stickel, M.E.: Complete sets of reductions for some equational theories. Journal of the ACM\u00a028, 233\u2013264 (1981)","journal-title":"Journal of the ACM"},{"key":"26_CR38","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS, vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"26_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48234-2_1","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"J. Rushby","year":"1999","unstructured":"Rushby, J.: Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem proving. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 311\u2013321. Springer, Heidelberg (1999)"},{"key":"26_CR40","series-title":"Lecture Notes in Artificial Intelligence","first-page":"391","volume-title":"Automated Deduction - CADE-18","author":"A. Stump","year":"2002","unstructured":"Stump, A., Dill, D.L.: Faster proof checking in the Edinburgh Logical Framework. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 391\u2013406. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,27]],"date-time":"2025-02-27T07:31:12Z","timestamp":1740641472000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}