{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:38:36Z","timestamp":1725489516519},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540731467"},{"type":"electronic","value":"9783540731474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73147-4_7","type":"book-chapter","created":{"date-parts":[[2007,8,17]],"date-time":"2007-08-17T04:01:50Z","timestamp":1187323310000},"page":"132-166","source":"Crossref","is-referenced-by-count":3,"title":["Superdeduction at Work"],"prefix":"10.1007","author":[{"given":"Paul","family":"Brauner","sequence":"first","affiliation":[]},{"given":"Cl\u00e9ment","family":"Houtmann","sequence":"additional","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Alvarado, C.: Reflection for rewriting in the calculus of inductive constructions. In: Proceedings of TYPES 2000, Durham, United Kingdom (December 2000)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-48242-3_20","volume-title":"Logic Programming and Automated Reasoning","author":"J.-M. Andreoli","year":"1999","unstructured":"Andreoli, J.-M., Maieli, R.: Focusing and proof-nets in linear and non-commutative logic. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol.\u00a01705, pp. 321\u2013336. Springer, Heidelberg (1999)"},{"issue":"3","key":"7_CR3","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation\u00a02(3), 297\u2013347 (1992)","journal-title":"Journal of Logic and Computation"},{"issue":"1-3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/S0168-0072(00)00032-4","volume":"107","author":"J.-M. Andreoli","year":"2001","unstructured":"Andreoli, J.-M.: Focussing and proof construction. Annals Pure Applied Logic\u00a0107(1-3), 131\u2013163 (2001)","journal-title":"Annals Pure Applied Logic"},{"key":"7_CR5","unstructured":"Brauner, P., Dowek, G., Wack, B.: Normalization in supernatural deduction and in deduction modulo (2007), Available at http:\/\/hal.inria.fr\/inria-00141720"},{"issue":"3-4","key":"7_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":"7_CR7","doi-asserted-by":"crossref","unstructured":"Brauner, P., Houtmann, C., Kirchner, C.: Principles of superdeduction. In: Proceedings of LICS (July 2007)","DOI":"10.1109\/LICS.2007.37"},{"issue":"1-2","key":"7_CR8","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0304-3975(00)00347-9","volume":"272","author":"F. Blanqui","year":"2002","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: Inductive Data Type Systems. Theoretical Computer Science\u00a0272(1-2), 41\u201368 (2002)","journal-title":"Theoretical Computer Science"},{"key":"7_CR9","unstructured":"Brauner, P.: Un calcul des s\u00e9quents extensible. Master\u2019s thesis, Universit\u00e9 Henri Poincar\u00e9 \u2013 Nancy 1 (2006)"},{"key":"7_CR10","unstructured":"Burel, G.: Unbounded proof-length speed-up in deduction modulo. Technical report, INRIA Lorraine (2007), Available at http:\/\/hal.inria.fr\/inria-00138195"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: TLCA 2007. LNCS, vol. 4583. Springer, Heidelberg (to appear, 2007)","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/351240.351262","volume-title":"ICFP \u201900: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP \u201900: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pp. 233\u2013243. ACM Press, New York, NY, USA (2000)"},{"issue":"3","key":"7_CR13","first-page":"427","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus \u2014 Part\u00a0I 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":"7_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"H. Cirstea","year":"2004","unstructured":"Cirstea, H., Liquori, L., Wack, B.: Rewriting calculus with fixpoints: Untyped and first-order systems. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, Springer, Heidelberg (2004)"},{"issue":"1","key":"7_CR15","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":"7_CR16","unstructured":"Dowek, G., Miquel, A.: Cut elimination for Zermelo\u2019s set theory. Available on author\u2019s web page (2007)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BFb0028389","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Dowek","year":"1997","unstructured":"Dowek, G.: Proof normalization for a first-order formulation of higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 105\u2013119. Springer, Heidelberg (1997)"},{"issue":"4","key":"7_CR18","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","volume":"68","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. Journal of Symbolic Logic\u00a068(4), 1289\u20131316 (2003)","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-3-540-32033-3_31","volume-title":"Term Rewriting and Applications","author":"G. Dowek","year":"2005","unstructured":"Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 423\u2013437. Springer, Heidelberg (2005)"},{"key":"7_CR20","unstructured":"Herbelin, H.: S\u00e9quents qu\u2019on calcule. PhD thesis, Universit\u00e9 Paris 7 (January 1995)"},{"key":"7_CR21","unstructured":"University of Cambridge, DSTO, SRI Internatioal. Description of the HOL-System (1993)"},{"key":"7_CR22","unstructured":"Houtmann, C.: Coh\u00e9rence de la d\u00e9duction surnaturelle. Master\u2019s thesis, \u00c9cole Normale Sup\u00e9rieure de Cachan (2006)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P.: Higher-order rewriting: Framework, confluence and termination. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R.C. (eds.) Processes, Terms and Cycles, pp. 224\u2013250 (2005)","DOI":"10.1007\/11601548_14"},{"key":"7_CR24","unstructured":"Kirchner, F.: A finite first-order theory of classes (2006) http:\/\/www.lix.polytechnique.fr\/Labo\/Florent.Kirchner\/"},{"key":"7_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1007\/11916277_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Kirchner","year":"2006","unstructured":"Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: Automatic combinability of rewriting-based satisfiability procedures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 542\u2013556. Springer, Heidelberg (2006)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. Electronic Notes in Theoretical Computer Science, vol. 86(4) (2003)","DOI":"10.1016\/S1571-0661(05)82619-2"},{"issue":"10","key":"7_CR27","doi-asserted-by":"publisher","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J. Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Information and Computation\u00a0204(10), 1575\u20131596 (2006)","journal-title":"Information and Computation"},{"key":"7_CR28","unstructured":"Moreau, P.-E., Reilles, A.: The tom home page (2006) http:\/\/tom.loria.fr"},{"issue":"3-4","key":"7_CR29","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":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"7_CR32","unstructured":"Prawitz, D.: Natural Deduction. A Proof-Theoretical Study, vol. 3 of Stockholm Studies in Philosophy. Almqvist & Wiksell, Stockholm (1965)"},{"key":"7_CR33","unstructured":"Prevosto, V.: Certified mathematical hierarchies: the focal system. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany (2005)"},{"key":"7_CR34","unstructured":"Rudnicki, P.: An overview of the Mizar project. Notes to a talk at the workshop on Types for Proofs and Programs (June 1992)"},{"key":"7_CR35","unstructured":"The Coq development team. The Coq proof assistant reference manual. LogiCal Project, Version 8.0 (2004)"},{"issue":"1-2","key":"7_CR36","first-page":"123","volume":"45","author":"C. Urban","year":"2001","unstructured":"Urban, C., Bierman, G.M.: Strong normalisation of cut-elimination in classical logic. Fundam. Inform.\u00a045(1-2), 123\u2013155 (2001)","journal-title":"Fundam. Inform."},{"key":"7_CR37","unstructured":"Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge, (October 2000)"},{"key":"7_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-45413-6_32","volume-title":"Typed Lambda Calculi and Applications","author":"C. Urban","year":"2001","unstructured":"Urban, C.: Strong normalisation for a gentzen-like cut-elimination procedure. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 415\u2013430. Springer, Heidelberg (2001)"},{"key":"7_CR39","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"WRLA","author":"E. Visser","year":"1998","unstructured":"Visser, E., Benaissa, Z.-e.-A.: A core language for rewriting. In: Kirchner, C., Kirchner, H. (eds.) WRLA, Pont-\u00e0-Mousson, France, September 1998. Electronic Notes in Theoretical Computer Science, vol.\u00a015, Elsevier, North-Holland (1998)"},{"key":"7_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/11560586_8","volume-title":"ICTCS 2005","author":"S. Bakel van","year":"2005","unstructured":"van Bakel, S., Lengrand, S., Lescanne, P.: The language \u03c7: circuits, computations and classical logic. In: van Bakel, S., Lengrand, S., Lescanne, P. (eds.) ICTCS 2005. Proceedings of Ninth Italian Conference on Theoretical Computer Science. LNCS, vol.\u00a03701, pp. 81\u201396. Springer, Heidelberg (2005)"},{"key":"7_CR41","unstructured":"Wack, B.: Typage et d\u00e9duction dans le calcul de r\u00e9\u00e9criture. PhD thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy 1 (October 2005)"},{"key":"7_CR42","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1145\/944705.944723","volume-title":"ICFP \u201903: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming","author":"P. Wadler","year":"2003","unstructured":"Wadler, P.: Call-by-value is dual to call-by-name. In: ICFP \u201903: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, September 2003, pp. 189\u2013201. ACM Press, New York (2003)"}],"container-title":["Lecture Notes in Computer Science","Rewriting, Computation and Proof"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73147-4_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:12:18Z","timestamp":1605762738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73147-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540731467","9783540731474"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73147-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}