{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:26:41Z","timestamp":1761596801194,"version":"3.41.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1023\/a:1021975117537","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"309-336","source":"Crossref","is-referenced-by-count":16,"title":["External Rewriting for Skeptical Proof Assistants"],"prefix":"10.1007","volume":"29","author":[{"given":"Quang Huy","family":"Nguyen","sequence":"first","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]},{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5109770_CR1","doi-asserted-by":"crossref","unstructured":"Abadi M., Cardelli, L., Curien, P.-L. and L\u00e9vy, J.-J.: Explicit substitutions, in ACM (ed.), Conf. Rec. 17th Symp. POPL, 1990, pp. 31\u201346.","DOI":"10.1145\/96709.96712"},{"key":"5109770_CR2","unstructured":"Alvarado, C. and Nguyen, Q.-H.: ELAN for equational reasoning in Coq, in J. Despeyroux (ed.), Proc. of LFM'00, INRIA, 2000. ISBN 2-7261-1166-1."},{"key":"5109770_CR3","unstructured":"Barendregt H. and Barendsen, E.: Autarkik computations in formal proofs, J. Symbolic Comput. (2002). To appear."},{"key":"5109770_CR4","doi-asserted-by":"crossref","first-page":"1149","DOI":"10.1016\/B978-044450813-3\/50020-5","volume-title":"Handbook of Automated Reasoning","author":"H. Barendregt","year":"2001","unstructured":"Barendregt, H. and Geuvers, H.: Proof-assistants using dependent type systems, in A. Robinson and A. Voronkov (eds), Handbook of Automated Reasoning, Vol. II, Elsevier Science Publishers B. V., North-Holland, 2001, Chapt. 18, pp. 1149\u20131238."},{"key":"5109770_CR5","doi-asserted-by":"crossref","unstructured":"Bezem M., Hendriks, D. and de Nivelle, H.: Automated proof construction in type theory using resolution, in D. McAllester (ed.), Proc. of CADE 17, LNAI 1831, 2000, pp. 148\u2013163.","DOI":"10.1007\/10721959_10"},{"key":"5109770_CR6","doi-asserted-by":"crossref","unstructured":"Blanqui, F.: Definitions by rewriting in the calculus of constructions, in Proc. of LICS'01, 2001, pp. 9\u201318.","DOI":"10.1109\/LICS.2001.932478"},{"key":"5109770_CR7","doi-asserted-by":"crossref","unstructured":"Boulton, R., Slind, K., Bundy, A. and Gordon, M.: An interface between CLAM and HOL, in J. Grundy and M. Newey (eds), Proc. of the 11th Int. Conf. TPHOL, LNCS 1479, 1998, pp. 87\u2013104.","DOI":"10.1007\/BFb0055131"},{"key":"5109770_CR8","doi-asserted-by":"crossref","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures, in M. Abadi and T. Ito (eds), Proc. of TAGS'97, LNCS 1281, 1997, pp. 515\u2013529.","DOI":"10.1007\/BFb0014565"},{"key":"5109770_CR9","unstructured":"Cirstea H.: Calcul de r\u00e9\u00e9criture: fondements et applications, Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9 \u2013 Nancy 1, 2000."},{"key":"5109770_CR10","first-page":"95","volume-title":"Frontiers of Combining Systems","author":"H. Cirstea","year":"1999","unstructured":"Cirstea, H. and Kirchner, C.: Combining higher-order and first-order computation using \u03c1-calculus: Towards a semantics of ELAN, in D. Gabbay and M. de Rijke (eds), Frontiers of Combining Systems 2, Research Studies, Wiley, 1999, pp. 95\u2013120."},{"issue":"3","key":"5109770_CR11","first-page":"427","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H. and Kirchner, C.: The rewriting calculus \u2013 Part I and II, J. Interest Group in Pure Appl. Logics\n9(3) (2001), 427\u2013498.","journal-title":"J. Interest Group in Pure Appl. Logics"},{"key":"5109770_CR12","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Kirchner, C. and Liquori, L.: The rho cube, in F. Honsell (ed.), Proc. of FOSSACS, LNCS 2030, 2001, pp. 166\u2013180.","DOI":"10.1007\/3-540-45315-6_11"},{"key":"5109770_CR13","doi-asserted-by":"crossref","unstructured":"Coquand, T. and Huet, G.: The calculus of constructions, Inform. Comput.\n76 (1988).","DOI":"10.1016\/0890-5401(88)90005-3"},{"issue":"2","key":"5109770_CR14","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"Curien, P.-L., Hardin, T. and Levy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions, J. ACM\n43(2) (1996), 362\u2013397.","journal-title":"J. ACM"},{"key":"5109770_CR15","unstructured":"Dowek, G., Hardin, T. and Kirchner, C.: Theorem proving modulo, Rapport de Recherche 3400, INRIA, 1998. Available at ftp:\/\/ftp.inria.fr\/INRIA\/publication\/RR\/RR-3400.ps.gz."},{"key":"5109770_CR16","unstructured":"Gadducci, F.: On the algebraic approach to concurrent term rewriting, Ph.D. thesis, Universit\u00e0 di Pisa, 1996."},{"key":"5109770_CR17","unstructured":"Harper, R., Honsell, F. and Plotkin, G.: A framework for defining logics, in Proc. of LICS'87, 1987, pp. 194\u2013204."},{"key":"5109770_CR18","series-title":"Technical Report","volume-title":"Metatheory and reflection in theorem proving: A survey and critique","author":"J. Harrison","year":"1995","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":"5109770_CR19","unstructured":"Hurd, J.: Integrating Gandalf and HOL, in Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin and L. Thery (eds), Proc. of TPHOLs'99, LNCS 1690, 1999, pp. 311\u201321."},{"issue":"4","key":"5109770_CR20","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P. and Kirchner, H.: Completion of a set of rules modulo a set of equations, SIAM J. Comput.\n15(4) (1986), 1155\u20131194.","journal-title":"SIAM J. Comput."},{"key":"5109770_CR21","unstructured":"Kirchner, C.: Computing unification algorithms, in Proc. of the 1st IEEE Symposium on Logic in Computer Science (USA), 1986, pp. 206\u2013216."},{"key":"5109770_CR22","doi-asserted-by":"crossref","unstructured":"Kirchner, C. and Klay, F.: Syntactic theories and unification, in Proc. of the 5th IEEE Symposium on Logic in Computer Science (USA), 1990, pp. 270\u2013277.","DOI":"10.1109\/LICS.1990.113753"},{"issue":"4","key":"5109770_CR23","doi-asserted-by":"crossref","first-page":"490","DOI":"10.1007\/BF01213535","volume":"8","author":"A. Martin","year":"1996","unstructured":"Martin, A., Gardiner, P. H. B. and Woodcock, J. C. P.: A tactic calculus \u2013 abridged version, Formal Aspects of Computing\n8(4) (1996), 490\u2013497.","journal-title":"Formal Aspects of Computing"},{"key":"5109770_CR24","doi-asserted-by":"crossref","unstructured":"Martin, U. and Nipkow, T.: Ordered rewriting and confluence, in M. Stickel (ed.), Proc. of CADE 10, LNCS 449, 1990, pp. 366\u2013380.","DOI":"10.1007\/3-540-52885-7_100"},{"issue":"1","key":"5109770_CR25","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency, Theoret. Comput. Sci.\n96(1) (1992), 73\u2013155.","journal-title":"Theoret. Comput. Sci."},{"key":"5109770_CR26","doi-asserted-by":"crossref","unstructured":"Necula, G. and Lee, P.: Efficient representation and validation of logical proofs, in Proc. of LICS'98, 1998, pp. 93\u2013104.","DOI":"10.1109\/LICS.1998.705646"},{"key":"5109770_CR27","unstructured":"Nguyen, Q.-H., Calcul de r\u00e9\u00e9criture et automatisation du raisonnement dans les assistants de preuve, Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9\u2013Nancy 1, 2002."},{"key":"5109770_CR28","unstructured":"Nguyen, Q.-H., Kirchner, C. and Kirchner, H.: External rewriting for skeptical proof assistants (extended version), Technical Report A02-R-099, LORIA, 2002. Available at http:\/\/www.loria.fr\/\u223cnguyenqh\/publication\/eatr.ps.gz."},{"key":"5109770_CR29","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Proof transformations for equational theories, in Proc. of the 5th IEEE Symposium on Logic in Computer Science (USA), 1990, pp. 278\u2013288.","DOI":"10.1109\/LICS.1990.113754"},{"key":"5109770_CR30","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq: Rules and properties, in M. Bezem and J. F. Groote (eds), Proc. of the 1st Int. Conf. TLCA, LNCS 664, Berlin, 1993, pp. 328\u2013345.","DOI":"10.1007\/BFb0037116"},{"issue":"3","key":"5109770_CR31","first-page":"73","volume":"5","author":"L. Paulson","year":"1999","unstructured":"Paulson, L.: A generic tableau prover and its integration with Isabelle, J. Universal Computer Sci.\n5(3) (1999), 73\u201387.","journal-title":"J. Universal Computer Sci."},{"key":"5109770_CR32","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"Peterson, G. and Stickel, M. E.: Complete sets of reductions for some equational theories, J. ACM\n28 (1981), 233\u2013264.","journal-title":"J. ACM"},{"key":"5109770_CR33","unstructured":"Ringeissen, C.: Combinaison de r\u00e9solutions de contraintes, Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9 \u2013 Nancy 1, 1993."},{"issue":"1&2","key":"5109770_CR34","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"Schmidt-Schau\u00df, M.: Unification in a combination of arbitrary disjoint equational theories, J. Symbolic Comput.\n8(1 & 2) (1989), 51\u201399.","journal-title":"J. Symbolic Comput."},{"key":"5109770_CR35","first-page":"391","volume":"2392","author":"A. Stump","year":"2002","unstructured":"Stump, A. and Dill, D. L.: Faster proof checking in the Edinburgh logical framework, in Proc. of CADE 18, LNCS 2392, 2002, pp. 391\u2013406.","journal-title":"Proc. of CADE 18"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021975117537.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021975117537\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021975117537.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:45:45Z","timestamp":1749123945000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021975117537"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":35,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109770"],"URL":"https:\/\/doi.org\/10.1023\/a:1021975117537","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}