{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T21:10:38Z","timestamp":1706649038405},"reference-count":17,"publisher":"Duke University Press","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Notre Dame J. Formal Logic"],"published-print":{"date-parts":[[2012,1,1]]},"DOI":"10.1215\/00294527-1722692","type":"journal-article","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T14:20:17Z","timestamp":1352384417000},"source":"Crossref","is-referenced-by-count":2,"title":["A Simple Proof that Super-Consistency Implies Cut Elimination"],"prefix":"10.1215","volume":"53","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[]},{"given":"Olivier","family":"Hermant","sequence":"additional","affiliation":[]}],"member":"73","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] Andrews, P. B., \u201cResolution in type theory,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 36 (1971), pp. 414\u201332.","DOI":"10.2307\/2269949"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] Church, A., \u201cA formulation of the simple theory of types,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 5 (1940), pp. 56\u201368.","DOI":"10.2307\/2266170"},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] De Marco, M., and J. Lipton, \u201cCompleteness and cut-elimination in the intuitionistic theory of types,\u201d <i>Journal of Logic and Computation<\/i>, vol. 15 (2005), pp. 821\u201354.","DOI":"10.1093\/logcom\/exi055"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] Dowek, G., \u201cTruth values algebras and proof normalization,\u201d pp. 110\u201324 in <i>Types for Proofs and Programs<\/i>, vol. 4502 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2007.","DOI":"10.1007\/978-3-540-74464-1_8"},{"key":"5","doi-asserted-by":"publisher","unstructured":"[5] Dowek, G., T. Hardin, and C. Kirchner, \u201cHOL-lambda-sigma: an intentional first-order expression of higher-order logic,\u201d pp. 21\u201345 in <i>Theory and Applications of Explicit Substitutions<\/i>, edited by D. Kesner, vol. 11 of <i>Mathematical Structures in Computer Science<\/i>, Cambridge University Press, Cambridge, 2001.","DOI":"10.1017\/S0960129500003236"},{"key":"6","doi-asserted-by":"publisher","unstructured":"[6] Dowek, G., T. Hardin, and C. Kirchner, \u201cTheorem proving modulo,\u201d <i>Journal of Automated Reasoning<\/i>, vol. 31 (2003), pp. 33\u201372.","DOI":"10.1023\/A:1027357912519"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] Dowek, G., and O. Hermant, \u201cA simple proof that super-consistency implies cut elimination,\u201d pp. 93\u2013106 in <i>Term Rewriting and Applications<\/i>, vol. 4533 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2007.","DOI":"10.1007\/978-3-540-73449-9_9"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[8] Dowek, G., and B. Werner, \u201cProof normalization modulo,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 68 (2003), pp. 1289\u20131316.","DOI":"10.2178\/jsl\/1067620188"},{"key":"9","doi-asserted-by":"crossref","unstructured":"[9] Girard, J.-Y., \u201cUne extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e0 l\u2019analyse et son application \u00e0 l\u2019\u00e9limination des coupures dans l\u2019analyse et la th\u00e9orie des types,\u201d pp. 63\u201392 in <i>Proceedings of the Second Scandinavian Logic Symposium (Oslo, 1970)<\/i>, vol. 63 of <i>Studies in Logic and the Foundations of Mathematics<\/i>, North-Holland, Amsterdam, 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] Hermant, O., and J. Lipton, \u201cA constructive semantic approach to cut elimination in type theories with axioms,\u201d pp. 169\u201383 in <i>Computer Science Logic<\/i>, vol. 5213 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2008.","DOI":"10.1007\/978-3-540-87531-4_14"},{"key":"11","doi-asserted-by":"publisher","unstructured":"[11] Hermant, O., and J. Lipton, \u201cCompleteness and cut-elimination in the intuitionistic theory of types, II,\u201d <i>Journal of Logic and Computation<\/i>, vol. 20 (2010), pp. 597\u2013602.","DOI":"10.1093\/logcom\/exp076"},{"key":"12","doi-asserted-by":"publisher","unstructured":"[12] Okada, M., \u201cA uniform semantic proof for cut-elimination and completeness of various first and higher order logics,\u201d <i>Theoretical Computer Science<\/i>, vol. 281 (2002), pp. 471\u201398.","DOI":"10.1016\/S0304-3975(02)00024-5"},{"key":"13","doi-asserted-by":"publisher","unstructured":"[13] Prawitz, D., \u201cHauptsatz for higher order logic,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 33 (1968), pp. 452\u201357.","DOI":"10.2307\/2270331"},{"key":"14","doi-asserted-by":"publisher","unstructured":"[14] Sch\u00fctte, K., \u201cSyntactical and semantical properties of simple type theory,\u201d <i>Journal of Symbolic Logic<\/i>, vol. 25 (1960), pp. 305\u201326.","DOI":"10.2307\/2963525"},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] Tait, W. W., \u201cA nonconstructive proof for Gentzen\u2019s Hauptsatz for second order predicate logic,\u201d <i>Bulletin of the American Mathematical Society<\/i>, vol. 72 (1966), pp. 980\u201383.","DOI":"10.1090\/S0002-9904-1966-11611-7"},{"key":"16","doi-asserted-by":"publisher","unstructured":"[16] Takahashi, M., \u201cA proof of cut-elimination theorem in simple type-theory,\u201d <i>Journal of the Mathematical Society of Japan<\/i>, vol. 19 (1967), pp. 399\u2013410.","DOI":"10.2969\/jmsj\/01940399"},{"key":"17","unstructured":"[17] Troelstra, A. S., and D. van Dalen, <i>Constructivism in Mathematics: An Introduction<\/i>, <i>Vol. I<\/i>, vol. 121 of <i>Studies in Logic and the Foundations of Mathematics<\/i>, North-Holland, Amsterdam, 1988. <i>Vol. II<\/i>, vol. 123 of <i>Studies in Logic and the Foundations of Mathematics<\/i>, North-Holland, Amsterdam, 1988."}],"container-title":["Notre Dame Journal of Formal Logic"],"original-title":[],"link":[{"URL":"https:\/\/projecteuclid.org\/journalArticle\/Download?urlid=10.1215\/00294527-1722692","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,30]],"date-time":"2024-01-30T20:57:55Z","timestamp":1706648275000},"score":1,"resource":{"primary":{"URL":"https:\/\/projecteuclid.org\/journals\/notre-dame-journal-of-formal-logic\/volume-53\/issue-4\/A-Simple-Proof-that-Super-Consistency-Implies-Cut-Elimination\/10.1215\/00294527-1722692.full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,1]]},"references-count":17,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2012,1,1]]}},"URL":"https:\/\/doi.org\/10.1215\/00294527-1722692","relation":{},"ISSN":["0029-4527"],"issn-type":[{"value":"0029-4527","type":"print"}],"subject":[],"published":{"date-parts":[[2012,1,1]]}}}