乐胖代购免代理版

{"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 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 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 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 Types for Proofs and Programs<\/i>, vol. 4502 of 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 Theory and Applications of Explicit Substitutions<\/i>, edited by D. Kesner, vol. 11 of 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 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 Term Rewriting and Applications<\/i>, vol. 4533 of 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 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 Proceedings of the Second Scandinavian Logic Symposium (Oslo, 1970)<\/i>, vol. 63 of 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 Computer Science Logic<\/i>, vol. 5213 of 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 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 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 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 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 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 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, Constructivism in Mathematics: An Introduction<\/i>, Vol. I<\/i>, vol. 121 of Studies in Logic and the Foundations of Mathematics<\/i>, North-Holland, Amsterdam, 1988. Vol. II<\/i>, vol. 123 of 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]]}}}