{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:13Z","timestamp":1763468113457},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357213"},{"type":"electronic","value":"9783642357220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35722-0_27","type":"book-chapter","created":{"date-parts":[[2013,1,4]],"date-time":"2013-01-04T11:16:29Z","timestamp":1357298189000},"page":"372-386","source":"Crossref","is-referenced-by-count":3,"title":["Contextual Natural Deduction"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Woltzenlogel Paleo","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-45220-1_9","volume-title":"Computer Science Logic","author":"K. Br\u00fcnnler","year":"2003","unstructured":"Br\u00fcnnler, K.: Atomic Cut Elimination for Classical Logic. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol.\u00a02803, pp. 86\u201397. Springer, Heidelberg (2003)"},{"key":"27_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-540-89439-1_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Br\u00fcnnler","year":"2008","unstructured":"Br\u00fcnnler, K., McKinley, R.: An Algorithmic Interpretation of a Deep Inference System. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 482\u2013496. Springer, Heidelberg (2008)"},{"key":"27_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1462179.1462186","volume":"10","author":"P. Bruscoli","year":"2009","unstructured":"Bruscoli, P., Guglielmi, A.: On the proof complexity of deep inference. ACM Transactions on Computational Logic\u00a010, 1\u201334 (2009)","journal-title":"ACM Transactions on Computational Logic"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-17511-4_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Bruscoli","year":"2010","unstructured":"Bruscoli, P., Guglielmi, A., Gundersen, T., Parigot, M.: A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 136\u2013153. Springer, Heidelberg (2010)"},{"key":"27_CR7","series-title":"Cahiers du Centre de Logique","volume-title":"The Curry-Howard Isomorphism","year":"1995","unstructured":"de Groote, P. (ed.): The Curry-Howard Isomorphism. Cahiers du Centre de Logique, vol.\u00a08. Academia, Universite Catholique de Louvain (1995)"},{"key":"27_CR8","unstructured":"Deharbe, D., Fontaine, P., Paleo, B.W.: Quantifier inference rules in the proof format of verit. In: 1st International Workshop on Proof Exchange for Theorem Proving (2011)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-01748-3_5","volume-title":"Languages: From Formal to Natural","author":"N. Dershowitz","year":"2009","unstructured":"Dershowitz, N.: On Lazy Commutation. In: Grumberg, O., Kaminski, M., Katz, S., Wintner, S. (eds.) Languages: From Formal to Natural. LNCS, vol.\u00a05533, pp. 59\u201382. Springer, Heidelberg (2009)"},{"key":"27_CR10","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1934-1935)","journal-title":"Mathematische Zeitschrift"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Guenot, N.: Nested proof search as reduction in the lambda-calculus. In: Schneider-Kamp, P., Hanus, M. (eds.) PPDP, pp. 183\u2013194. ACM (2011)","DOI":"10.1145\/2003476.2003501"},{"key":"27_CR12","unstructured":"Guglielmi, A.: A system of interaction and structure. CoRR, cs.LO\/9910023 (1999)"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-28717-6_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Hetzl","year":"2012","unstructured":"Hetzl, S., Leitsch, A., Weller, D.: Towards Algorithmic Cut-Introduction. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 228\u2013242. Springer, Heidelberg (2012)"},{"issue":"1","key":"27_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comput. Sci.\u00a0192(1), 3\u201329 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb\u03bc-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"27_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/11916277_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A.F. Tiu","year":"2006","unstructured":"Tiu, A.F.: A Local System for Intuitionistic Logic. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 242\u2013256. Springer, Heidelberg (2006)"},{"key":"27_CR17","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-17511-4_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B. Woltzenlogel Paleo","year":"2010","unstructured":"Woltzenlogel Paleo, B.: Atomic Cut Introduction by Resolution: Proof Structuring and Compression. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS (LNAI), vol.\u00a06355, pp. 463\u2013480. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35722-0_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T13:24:28Z","timestamp":1620134668000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35722-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642357213","9783642357220"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35722-0_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}