{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T02:19:53Z","timestamp":1725761993694},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642452208"},{"type":"electronic","value":"9783642452215"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_28","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"407-422","source":"Crossref","is-referenced-by-count":0,"title":["Semantic A-translations and Super-Consistency Entail Classical Cut Elimination"],"prefix":"10.1007","author":[{"given":"Lisa","family":"Allali","sequence":"first","affiliation":[]},{"given":"Olivier","family":"Hermant","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The \u03bb\u03a0-Calculus Modulo as a Universal Proof Language. In: Proof Exchange for Theorem Proving (PxTP), Manchester, UK, pp. 28\u201343 (June 2012)"},{"key":"28_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-540-25984-8_33","volume-title":"Automated Reasoning","author":"R. Bonichon","year":"2004","unstructured":"Bonichon, R.: TaMeD: A tableau method for deduction modulo. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 445\u2013459. Springer, Heidelberg (2004)"},{"key":"28_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11916277_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Bonichon","year":"2006","unstructured":"Bonichon, R., Hermant, O.: A Semantic Completeness Proof for TaMeD. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Brunel, A., Hermant, O., Houtmann, C.: Orthogonality and boolean algebras for deduction modulo. In: Ong, L. (ed.) TLCA 2011. LNCS, vol.\u00a06690, pp. 76\u201390. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-21691-6_9"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-15205-4_15","volume-title":"Computer Science Logic","author":"G. Burel","year":"2010","unstructured":"Burel, G.: Embedding Deduction Modulo into a Prover. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 155\u2013169. Springer, Heidelberg (2010)"},{"issue":"2","key":"28_CR6","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/j.ic.2009.10.005","volume":"208","author":"G. Burel","year":"2010","unstructured":"Burel, G., Kirchner, C.: Regaining cut admissibility in deduction modulo using abstract completion. Inf. Comput.\u00a0208(2), 140\u2013164 (2010)","journal-title":"Inf. Comput."},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-540-74464-1_8","volume-title":"Types for Proofs and Programs","author":"G. Dowek","year":"2007","unstructured":"Dowek, G.: Truth values algebras and proof normalization. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 110\u2013124. Springer, Heidelberg (2007)"},{"issue":"1","key":"28_CR8","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":"4","key":"28_CR9","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1215\/00294527-1722692","volume":"53","author":"G. Dowek","year":"2012","unstructured":"Dowek, G., Hermant, O.: A simple proof that super-consistency implies cut elimination. Notre-Dame Journal of Formal Logic\u00a053(4), 439\u2013456 (2012)","journal-title":"Notre-Dame Journal of Formal Logic"},{"issue":"4","key":"28_CR10","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. The Journal of Symbolic Logic\u00a068(4), 1289\u20131316 (2003)","journal-title":"The Journal of Symbolic Logic"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"28_CR12","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BFb0103100","volume-title":"Higher Set Theory","author":"H. Friedman","year":"1978","unstructured":"Friedman, H.: Classically and intuitionistically provably recursive functions. In: M\u00fcller, G.H., Scott, D.S. (eds.) MPC 1992. Lecture Notes in Mathematics, vol.\u00a0669, pp. 21\u201327. Springer, Heidelberg (1978)"},{"key":"28_CR13","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/BF01565428","volume":"112","author":"G. Gentzen","year":"1936","unstructured":"Gentzen, G.: Die widerspruchsfreiheit der reinen zahlentheorie. Mathematische Annalen\u00a0112, 493\u2013565 (1936)","journal-title":"Mathematische Annalen"},{"key":"28_CR14","first-page":"34","volume":"4","author":"K. G\u00f6del","year":"1933","unstructured":"G\u00f6del, K.: Zur intuitionistischen arithmetik und zahlentheorie. Ergebnisse Eines Mathematischen Kolloquiums\u00a04, 34\u201338 (1933)","journal-title":"Ergebnisse Eines Mathematischen Kolloquiums"},{"issue":"1","key":"28_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1182613.1182614","volume":"8","author":"A. Guglielmi","year":"2007","unstructured":"Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Log.\u00a08(1), 1\u201364 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11417170_17","volume-title":"Typed Lambda Calculi and Applications","author":"O. Hermant","year":"2005","unstructured":"Hermant, O.: Semantic cut elimination in the intuitionistic sequent calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 221\u2013233. Springer, Heidelberg (2005)"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-87531-4_14","volume-title":"Computer Science Logic","author":"O. Hermant","year":"2008","unstructured":"Hermant, O., Lipton, J.: A constructive semantic approach to cut elimination in type theories with axioms. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 169\u2013183. Springer, Heidelberg (2008)"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-31365-3_26","volume-title":"Automated Reasoning","author":"M. Jacquel","year":"2012","unstructured":"Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 332\u2013338. Springer, Heidelberg (2012)"},{"key":"28_CR19","unstructured":"TeReSe. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press (2003)"},{"key":"28_CR20","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, An Introduction. North-Holland (1988)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45221-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T04:19:12Z","timestamp":1558757952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}