{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T22:07:09Z","timestamp":1759615629514,"version":"3.37.3"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T00:00:00Z","timestamp":1550448000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s11225-019-09847-4","type":"journal-article","created":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T12:55:54Z","timestamp":1550494554000},"page":"291-357","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Normality, Non-contamination and Logical Depth in Classical Natural Deduction"],"prefix":"10.1007","volume":"108","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3832-4487","authenticated-orcid":false,"given":"Marcello","family":"D\u2019Agostino","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dov","family":"Gabbay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjay","family":"Modgil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,2,18]]},"reference":[{"key":"9847_CR1","doi-asserted-by":"crossref","unstructured":"Aschieri, F., A.\u00a0Ciabattoni, and F.A. Genco, Classical proofs as parallel programs, in A. Orlandini, and M.\u00a0Zimmermann, (eds.), Proceedings of the 9th Symposium on Games, Automata, Logics and Formal Verification (GandALF\u201918), vol. 277 of EPTCS, 2018, pp. 43\u201357.","DOI":"10.4204\/EPTCS.277.4"},{"key":"9847_CR2","first-page":"10","volume":"171","author":"TJM Bench-Capon","year":"2007","unstructured":"Bench-Capon, T.J.M., and P.E. Dunne, Argumentation in artificial intelligence. Artificial intelligence 171:10\u201315, 2007.","journal-title":"Artificial intelligence"},{"key":"9847_CR3","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/BF00245930","volume":"7","author":"K Bendall","year":"1978","unstructured":"Bendall, K., Natural deduction, separation and the meaning of logical operators. Journal of Philosophical Logic 7:245\u2013276, 1978.","journal-title":"Journal of Philosophical Logic"},{"key":"9847_CR4","doi-asserted-by":"publisher","first-page":"197","DOI":"10.2307\/2184181","volume":"78","author":"J Bennett","year":"1969","unstructured":"Bennett, J., Entailment. The Philosophical Review 78:197\u2013236, 1969.","journal-title":"The Philosophical Review"},{"issue":"5\u20136","key":"9847_CR5","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1016\/j.artint.2007.02.003","volume":"171","author":"M Caminada","year":"2007","unstructured":"Caminada, M., and L. Amgoud, On the evaluation of argumentation formalisms. Artificial Intelligence 171(5-6):286\u2013310, 2007.","journal-title":"Artificial Intelligence"},{"issue":"5","key":"9847_CR6","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1093\/logcom\/exr033","volume":"22","author":"M Caminada","year":"2012","unstructured":"Caminada, M., W.\u00a0Carnielli, and P.\u00a0Dunne, Semi-stable semantics. Journal of Logic and Computation 22(5):1207\u20131254, 2012.","journal-title":"Journal of Logic and Computation"},{"key":"9847_CR7","volume-title":"Investigations into the Complexity of some Propositional calculi","author":"M D\u2019Agostino","year":"1990","unstructured":"D\u2019Agostino, M., Investigations into the Complexity of some Propositional calculi. Oxford University Computing Laboratory, Oxford, 1990."},{"key":"9847_CR8","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/BF00156916","volume":"1","author":"M D\u2019Agostino","year":"1992","unstructured":"D\u2019Agostino, M., Are tableaux an improvement on truth tables? Cut-free proofs and bivalence. Journal of Logic, Language and Information 1:235\u2013252, 1992.","journal-title":"Journal of Logic, Language and Information"},{"key":"9847_CR9","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-94-017-1754-0_2","volume-title":"Handbook of Tableau Methods","author":"M D\u2019Agostino","year":"1999","unstructured":"D\u2019Agostino, M., Tableau methods for classical propositional logic, in M. D\u2019Agostino, D.M. Gabbay, R.\u00a0H\u00e4hnle, and J.\u00a0Posegga, (eds.), Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht, 1999, pp. 45\u2013123."},{"key":"9847_CR10","first-page":"429","volume-title":"We Will Show Them!","author":"M D\u2019Agostino","year":"2005","unstructured":"D\u2019Agostino, M., Classical natural deduction, in S.N. Art\u00ebmov, H.\u00a0Barringer, A.S. d\u2019Avila Garceza, L.C. Lamb, and J.\u00a0Woods, (eds.), We Will Show Them!, vol.\u00a01, College Publications, London, 2005, pp. 429\u2013468."},{"key":"9847_CR11","first-page":"407","volume":"227","author":"M D\u2019Agostino","year":"2014","unstructured":"D\u2019Agostino, M., Analytic inference and the informational meaning of the logical operators. Logique et Analyse 227:407\u2013437, 2014.","journal-title":"Logique et Analyse"},{"key":"9847_CR12","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.tcs.2015.06.057","volume":"606","author":"M D\u2019Agostino","year":"2015","unstructured":"D\u2019Agostino, M., An informational view of classical logic. Theoretical Computer Science 606:79\u201397, 2015.","journal-title":"Theoretical Computer Science"},{"key":"9847_CR13","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.tcs.2013.02.014","volume":"480","author":"M D\u2019Agostino","year":"2013","unstructured":"D\u2019Agostino, M., M.\u00a0Finger, and D.M. Gabbay, Semantics and proof-theory of Depth-Bounded Boolean Logics. Theoretical Computer Science 480:43\u201368, 2013.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"9847_CR14","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s11229-008-9409-4","volume":"167","author":"M D\u2019Agostino","year":"2009","unstructured":"D\u2019Agostino, M., and L.\u00a0Floridi, The enduring scandal of deduction. Is propositional logic really uninformative? Synthese 167(2):271\u2013315, 2009.","journal-title":"Synthese"},{"key":"9847_CR15","unstructured":"D\u2019Agostino, M., and S.\u00a0Modgil, A rational account of classical logic argumentation for real-world agents, in Proceedings of European Conference on Artificial Intelligence (ECAI\u201916), IOS Press, 2016, pp. 141\u2013149."},{"key":"9847_CR16","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.artint.2018.05.003","volume":"262","author":"M D\u2019Agostino","year":"2018","unstructured":"D\u2019Agostino, M., and S.\u00a0Modgil, Classical logic, argument and dialectic. Artificial Intelligence 262:15\u201351, 2018.","journal-title":"Artificial Intelligence"},{"issue":"3","key":"9847_CR17","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M D\u2019Agostino","year":"1994","unstructured":"D\u2019Agostino, M., and M.\u00a0Mondadori, The taming of the cut. Classical refutations with analytic cut. Journal of Logic and Computation 4(3):285\u2013319, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"9847_CR18","volume-title":"The logical basis of metaphysics","author":"M Dummett","year":"1991","unstructured":"Dummett, M., The logical basis of metaphysics. Duckworth, London, 1991."},{"issue":"2","key":"9847_CR19","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0004-3702(94)00041-X","volume":"77","author":"PM Dung","year":"1995","unstructured":"Dung, P.M., On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence 77(2):321\u2013358, 1995.","journal-title":"Artificial Intelligence"},{"key":"9847_CR20","doi-asserted-by":"crossref","unstructured":"Ferrari, M., and C.\u00a0Fiorentini, Proof search in natural deduction calculus for classical propositional logic, in H.\u00a0De\u00a0Nivelle, (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, number 9323 in Lecture Notes in Artificial Intelligence, Berlin, Springer, 2015, pp. 237\u2013252.","DOI":"10.1007\/978-3-319-24312-2_17"},{"key":"9847_CR21","first-page":"1051","volume":"117","author":"F Ferreira","year":"2008","unstructured":"Ferreira, F., The coordination principle. A problem for bilateralism. Mind 117:1051\u20131057, 2008.","journal-title":"A problem for bilateralism. Mind"},{"key":"9847_CR22","volume-title":"Symbolic Logic: an Introduction","author":"FB Fitch","year":"1952","unstructured":"Fitch, F.B., Symbolic Logic: an Introduction. The Ronald Press Company, New York, 1952."},{"key":"9847_CR23","doi-asserted-by":"publisher","first-page":"s108","DOI":"10.1016\/j.jal.2017.11.001","volume":"25","author":"M Gabbay","year":"2017","unstructured":"Gabbay, M., Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons). Journal of Applied Logic 25:s108\u2013s122, 2017.","journal-title":"Journal of Applied Logic"},{"key":"9847_CR24","doi-asserted-by":"crossref","unstructured":"Gentzen, G., Unstersuchungen \u00fcber das logische Schliessen. Math. Zeitschrift, 39:176\u2013210, 1935. English translation in Szabo [1969].","DOI":"10.1007\/BF01201353"},{"key":"9847_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11225-014-9564-1","volume":"102","author":"AP Hazen","year":"2014","unstructured":"Hazen, A.P., and F.J. Pelletier, Gentzen and Ja\u015bkowski natural deduction: fundamentally similar but importantly different. Studia Logica 102:1\u201340, 2014.","journal-title":"Studia Logica"},{"key":"9847_CR26","volume-title":"Logic, Language Games and Information: Kantian Themes in the Philosophy of Logic","author":"J Hintikka","year":"1972","unstructured":"Hintikka, J., Logic, Language Games and Information: Kantian Themes in the Philosophy of Logic. Oxford University Press, Oxford, 1972."},{"key":"9847_CR27","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1023\/A:1004747920321","volume":"29","author":"L Humberstone","year":"2000","unstructured":"Humberstone, L., The revival of rejective negation. Journal of Philosophical Logic 29:331\u2013381, 2000.","journal-title":"Journal of Philosophical Logic"},{"key":"9847_CR28","doi-asserted-by":"crossref","unstructured":"Indrzejczak, A., Natural Deduction, Hybrid Systems and Modal Logics. Trends in Logic 30. Springer, Dordrecht, 1 edition, 2010.","DOI":"10.1007\/978-90-481-8785-0_1"},{"key":"9847_CR29","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s11225-017-9736-x","volume":"106","author":"A Kakas","year":"2018","unstructured":"Kakas, A., P. Mancarella, and F. Toni, On argumentation logic and propositional logic. Studia Logica 106:237\u2013279, 2018.","journal-title":"Studia Logica"},{"key":"9847_CR30","volume-title":"Mathematical Logic","author":"SC Kleene","year":"1967","unstructured":"Kleene, S.C., Mathematical Logic. John Wiley & Sons, Inc., New York, 1967."},{"key":"9847_CR31","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1093\/jigpal\/jzt038","volume":"22","author":"D Makinson","year":"2013","unstructured":"Makinson, D., On an inferential semantics for classical logic. Logic Journal of IGPL 22:147\u2013154, 2013.","journal-title":"Logic Journal of IGPL"},{"key":"9847_CR32","first-page":"79","volume":"23","author":"M Mareti\u0107","year":"2018","unstructured":"Mareti\u0107, M., On multiple conclusion deductions in classical logic. Mathematical Communications 23:79\u201395, 2018.","journal-title":"Mathematical Communications"},{"key":"9847_CR33","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1016\/j.artint.2012.10.008","volume":"195","author":"S Modgil","year":"2013","unstructured":"Modgil, S., and H.\u00a0Prakken. A general account of argumentation and preferences. Artificial Intelligence 195(0):361\u2013397, 2013.","journal-title":"Artificial Intelligence"},{"key":"9847_CR34","volume-title":"Chapter 21 in Handbook of Agreement Technologies","author":"S Modgil","year":"2013","unstructured":"Modgil, S., F.\u00a0Toni, F.\u00a0Bex, I.\u00a0Bratko, C.I. Chesnevar, X.\u00a0Fan, S.\u00a0Gaggl, A.J. Garcia, M.P. Gonzalez, T.\u00a0Gordon, J.\u00a0Leite, M.\u00a0Mozina, C.\u00a0Reed, G.R. Simari, S.\u00a0Szeider, P.\u00a0Torroni, and S.\u00a0Woltran, The added value of argumentation: Examples and challenges, in S. Ossowski, (ed.), Chapter 21 in Handbook of Agreement Technologies. Springer, New York, 2013."},{"key":"9847_CR35","unstructured":"Mondadori, M., Classical analytical deduction. Annali dell\u2019Universit\u00e0 di Ferrara; Sez. III; Discussion paper\u00a01, Universit\u00e0 di Ferrara, 1988."},{"key":"9847_CR36","unstructured":"Mondadori, M., On the notion of a classical proof. In Temi e prospettive della logica e della filosofia della scienza contemporanee, volume\u00a0I, Bologna, CLUEB, 1988 pp. 211\u2013224."},{"key":"9847_CR37","unstructured":"Mondadori, M., An improvement of Jeffrey\u2019s deductive trees. Annali dell\u2019Universit\u00e0 di Ferrara; Sez. III; Discussion paper\u00a07, Universit\u00e0 di Ferrara, 1989."},{"issue":"6","key":"9847_CR38","doi-asserted-by":"publisher","first-page":"939","DOI":"10.1093\/jigpal\/3.6.939","volume":"3","author":"M Mondadori","year":"1995","unstructured":"Mondadori, M., Efficient inverse tableaux. Logic Journal of the IGPL 3(6):939\u2013953, 1995.","journal-title":"Logic Journal of the IGPL"},{"key":"9847_CR39","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S Negri","year":"2001","unstructured":"Negri, S., and J.\u00a0von Plato, Structural Proof Theory. Cambridge University Press, New York, 2001."},{"key":"9847_CR40","doi-asserted-by":"crossref","unstructured":"Pelletier, F.J., and A.P. Hazen, A history of natural deduction, in D.M. Gabbay, J.F. Pelletier, and J.\u00a0Woods, (eds.), Handbook of the History of Logic, volume 11: Logic. A History of its Central Concepts. Elsevier, Amsterdam, 2012.","DOI":"10.1016\/B978-0-444-52937-4.50007-1"},{"key":"9847_CR41","volume-title":"Natural Deduction. A Proof-Theoretical Study.","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D. Natural Deduction. A Proof-Theoretical Study. Almqvist & Wilksell, Uppsala, 1965."},{"key":"9847_CR42","volume-title":"The Roots of Reference","author":"WVO Quine","year":"1973","unstructured":"Quine, W.V.O., The Roots of Reference. Open Court, La Salle, Illinois, 1973."},{"key":"9847_CR43","first-page":"91","volume":"8","author":"A Raggio","year":"1965","unstructured":"Raggio, A., Gentzen\u2019s Hauptsatz for the systems NI and NK. Logique et Analyse 8:91\u2013100, 1965.","journal-title":"Logique et Analyse"},{"key":"9847_CR44","doi-asserted-by":"publisher","first-page":"781","DOI":"10.1093\/mind\/109.436.781","volume":"109","author":"I Rumfit","year":"2000","unstructured":"Rumfit, I., \u201cYes\u201d and \u201cNo\u201d. Mind 109:781\u2013823, 2000.","journal-title":"Mind"},{"key":"9847_CR45","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1093\/analys\/anp003","volume":"69","author":"T Sandqvist","year":"2009","unstructured":"Sandqvist, T., Classical logic without bivalence. Analysis 69:211\u2013218, 2009.","journal-title":"Analysis"},{"key":"9847_CR46","doi-asserted-by":"crossref","unstructured":"Sieg, W., and F.\u00a0Pfenning, (eds.), Special Issue of Studia Logica on Automated Natural Deduction, vol.\u00a060, 1998.","DOI":"10.1023\/A:1005065031956"},{"key":"9847_CR47","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/analys\/56.1.1","volume":"56","author":"T Smiley","year":"1996","unstructured":"Smiley, T., Rejection. Analysis 56:1\u20139, 1996.","journal-title":"Analysis"},{"issue":"2","key":"9847_CR48","doi-asserted-by":"publisher","first-page":"123","DOI":"10.2307\/2270130","volume":"30","author":"R Smullyan","year":"1965","unstructured":"Smullyan, R., Analytic natural deduction. Journal of Symbolic Logic 30(2):123\u2013139, 1965.","journal-title":"Journal of Symbolic Logic"},{"key":"9847_CR49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R Smullyan","year":"1968","unstructured":"Smullyan, R., First-Order Logic. Springer, Berlin, 1968."},{"key":"9847_CR50","unstructured":"Statman, R., Structural Complexity of Proofs. Ph.D. thesis, University of Stanford, 1974."},{"key":"9847_CR51","doi-asserted-by":"publisher","first-page":"129","DOI":"10.2307\/2274910","volume":"56","author":"G St\u00e5lmarck","year":"1991","unstructured":"St\u00e5lmarck, G., Normalization theorems for full first order classical natural deduction. The Journal of Symbolic Logic 56:129\u2013149, 1991.","journal-title":"The Journal of Symbolic Logic"},{"volume-title":"The Collected Papers of Gerhard Gentzen","year":"1969","key":"9847_CR52","unstructured":"Szabo, M., (ed.), The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969."},{"key":"9847_CR53","first-page":"179","volume":"XLIII","author":"N Tennant","year":"1984","unstructured":"Tennant, N., Perfect validity, entailment and paraconsistency. Studia Logica XLIII:179\u2013198, 1984.","journal-title":"Studia Logica"},{"issue":"3","key":"9847_CR54","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1017\/S0022481200029674","volume":"52","author":"N Tennant","year":"1987","unstructured":"Tennant, N., Natural deduction and sequent calculus for intuitionistic relevant logic. Journal of Symbolic Logic 52(3):665\u2013680, 1987.","journal-title":"Journal of Symbolic Logic"},{"key":"9847_CR55","volume-title":"Natural Logic","author":"N Tennant","year":"1990","unstructured":"Tennant, N., Natural Logic. Edinburgh University Press, Edinburgh, 1990."},{"key":"9847_CR56","volume-title":"Autologic","author":"N Tennant","year":"1992","unstructured":"Tennant, N., Autologic. Edinburgh University Press, Edinburgh, 1992."},{"issue":"4","key":"9847_CR57","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A., The complexity of propositional proofs. Bulletin of Symbolic Logic 1 (4):425\u2013467, 1995.","journal-title":"Bulletin of Symbolic Logic"},{"issue":"2","key":"9847_CR58","doi-asserted-by":"publisher","first-page":"240","DOI":"10.2178\/bsl\/1208442829","volume":"14","author":"J Plato von","year":"2008","unstructured":"von Plato, J., Gentzen\u2019s proof of normalization for natural deduction. Bulletin of Symbolic Logic 14(2):240\u2013257, 2008.","journal-title":"Bulletin of Symbolic Logic"},{"key":"9847_CR59","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1017\/S1755020311000311","volume":"5","author":"J Plato von","year":"2012","unstructured":"von Plato, J., and A.\u00a0Siders, Normal derivability in classical natural deduction. The Review of Symbolic Logic 5:205\u2013211, 2012.","journal-title":"The Review of Symbolic Logic"},{"key":"9847_CR60","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-11041-7","volume-title":"Dag Prawitz on Proofs and Meaning","author":"H Wansing","year":"2015","unstructured":"Wansing, H., Prawitz, proofs and meaning, in H.\u00a0Wansing, (ed.), Dag Prawitz on Proofs and Meaning, Springer, New York, 2015, pp. 1\u201332."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-019-09847-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-019-09847-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-019-09847-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T18:51:11Z","timestamp":1694631071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-019-09847-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,18]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["9847"],"URL":"https:\/\/doi.org\/10.1007\/s11225-019-09847-4","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2019,2,18]]},"assertion":[{"value":"23 March 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 February 2019","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}