{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:23:06Z","timestamp":1740108186150,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"7-8","license":[{"start":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T00:00:00Z","timestamp":1614124800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T00:00:00Z","timestamp":1614124800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP16K16689"],"award-info":[{"award-number":["JP16K16689"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2021,11]]},"DOI":"10.1007\/s00153-020-00759-y","type":"journal-article","created":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T18:02:58Z","timestamp":1614189778000},"page":"783-813","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization"],"prefix":"10.1007","volume":"60","author":[{"given":"Ryo","family":"Takemura","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,2,24]]},"reference":[{"key":"759_CR1","doi-asserted-by":"crossref","unstructured":"Allwein, G., Barwise, J. (eds). Logical reasoning with diagrams. Oxford Studies. In: Logic And Computation Series (1996)","DOI":"10.1093\/oso\/9780195104271.001.0001"},{"key":"759_CR2","volume-title":"Logical Reasoning With Diagrams & Sentences: Using Hyperproof","author":"D Barker-Plummer","year":"2017","unstructured":"Barker-Plummer, D., Barwise, J., Etchemendy, J.: Logical Reasoning With Diagrams & Sentences: Using Hyperproof. CSLI Publications, Stanford (2017)"},{"issue":"3","key":"759_CR3","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1080\/09528130701475401","volume":"19","author":"D Barker-Plummer","year":"2007","unstructured":"Barker-Plummer, D., Etchemendy, J.: A computational architecture for heterogeneous reasoning. J. Exp. Theor. Artif. Intell. 19(3), 195\u2013225 (2007)","journal-title":"J. Exp. Theor. Artif. Intell."},{"issue":"1","key":"759_CR4","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.jvlc.2010.11.006","volume":"22","author":"D Barker-Plummer","year":"2011","unstructured":"Barker-Plummer, D., Swoboda, N.: Reasoning with coincidence grids-A sequent-based logic and an analysis of complexity. J. Vis. Lang. Comput. 22(1), 56\u201365 (2011)","journal-title":"J. Vis. Lang. Comput."},{"key":"759_CR5","unstructured":"Barwise, J., Etchemendy, J.: Hyperproof: For Macintosh. The Center for the Study of Language and Information Publications (1995)"},{"key":"759_CR6","unstructured":"Dyckhoff, R.: Implementing a simple proof assistant. In: Proceedings of the Workshop on Programming for Logic Teaching, Leeds Centre for Theoretical Computer Science Proceedings 23(88), pp. 49\u201359 (1988)"},{"key":"759_CR7","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift 39 176\u2013210, 405\u2013431 (1934). English Translation: Investigations into logical deduction, in M. E. Szabo, ed., The collected Papers of Gerhard Gentzen (1969)"},{"issue":"1","key":"759_CR8","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1305\/ndjfl\/1040609295","volume":"35","author":"E Hammer","year":"1994","unstructured":"Hammer, E.: Reasoning with sentences and diagrams. Notre Dame J. Formal Logic 35(1), 73\u201387 (1994)","journal-title":"Notre Dame J. Formal Logic"},{"key":"759_CR9","doi-asserted-by":"crossref","unstructured":"Howse, J., Stapleton, G., Taylor, J.: Spider Diagrams. LMS Journal of Computation and Mathematics, Volume 8, 145\u2013194, London Mathematical Society (2005)","DOI":"10.1112\/S1461157000000942"},{"key":"759_CR10","volume-title":"Mental Models: Toward a Cognitive Science of Language, Inference and Consciousness","author":"PN Johnson-Laird","year":"1983","unstructured":"Johnson-Laird, P.N.: Mental Models: Toward a Cognitive Science of Language, Inference and Consciousness. Harvard University Press, Boston (1983)"},{"key":"759_CR11","unstructured":"L\u00f3pez-Escobar, E.G.K.: Standardizing the N systems of Gentzen. In: Models, algebras, and proofs, Caicedo, X., Montenegro, C., (eds), Lecture Notes in Pure and Applied Mathematics, vol. 203, pp. 411\u2013434 (1999)"},{"issue":"3","key":"759_CR12","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/s10849-012-9160-6","volume":"21","author":"K Mineshima","year":"2012","unstructured":"Mineshima, K., Okada, M., Takemura, R.: A Diagrammatic Inference System with Euler Circles. J. Logic Lang. Inf. 21(3), 365\u2013391 (2012)","journal-title":"J. Logic Lang. Inf."},{"key":"759_CR13","doi-asserted-by":"crossref","unstructured":"Mineshima, K., Okada, M., Takemura, R.: Two Types of diagrammatic inference systems: natural deduction style and resolution style. diagrammatic representation and inferenc. In: 6th International Conference, Diagrams 2010, Lecture Notes In Artificial Intelligence, Springer, pp. 99\u2013114 (2010)","DOI":"10.1007\/978-3-642-14600-8_12"},{"key":"759_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S Negri","year":"2001","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)"},{"volume-title":"Advances in Proof-Theoretic Semantics","year":"2016","key":"759_CR15","unstructured":"Piecha, T., Schroeder-Heister, P. (eds.): Advances in Proof-Theoretic Semantics. Springer, Berlin (2016)"},{"key":"759_CR16","volume-title":"Natural Deduction, Almqvist & Wiksell, 1965","author":"D Prawitz","year":"2006","unstructured":"Prawitz, D.: Natural Deduction, Almqvist & Wiksell, 1965. Dover, Mineola (2006)"},{"key":"759_CR17","doi-asserted-by":"crossref","unstructured":"Prawitz, D.: Ideas and results in proof theory. In: Proceedings 2nd Scandinavian Logic Symposium, pp. 237\u2013309 (1971)","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"759_CR18","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5680.001.0001","volume-title":"The Psychology of Proof: Deductive Reasoning in Human Thinking","author":"LJ Rips","year":"1994","unstructured":"Rips, L.J.: The Psychology of Proof: Deductive Reasoning in Human Thinking. MIT Press, Cambridge (1994)"},{"issue":"4","key":"759_CR19","doi-asserted-by":"publisher","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"P Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister, P.: A natural extension of natural deduction. J. Symb. Logic 49(4), 1284\u20131300 (1984)","journal-title":"J. Symb. Logic"},{"issue":"3","key":"759_CR20","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/s11229-004-6296-1","volume":"148","author":"P Schroeder-Heister","year":"2006","unstructured":"Schroeder-Heister, P.: Validity concepts in proof-theoretic semantics. Synthese 148(3), 525\u2013571 (2006)","journal-title":"Synthese"},{"key":"759_CR21","volume-title":"The Logical Status of Diagrams","author":"S-J Shin","year":"1994","unstructured":"Shin, S.-J.: The Logical Status of Diagrams. Cambridge University Press, Cambridge (1994)"},{"key":"759_CR22","volume-title":"Semantic Properties of Diagrams and Their Cognitive Potentials","author":"A Shimojima","year":"2015","unstructured":"Shimojima, A.: Semantic Properties of Diagrams and Their Cognitive Potentials. CSLI Publications, Stanford (2015)"},{"key":"759_CR23","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.entcs.2005.02.023","volume":"134","author":"N Swoboda","year":"2005","unstructured":"Swoboda, N., Allwein, G.: Heterogeneous reasoning with Euler\/Venn diagrams containing named constants and FOL. Electron. Notes Theor. Comput. Sci. 134, 153\u2013187 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"759_CR24","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s11225-012-9370-6","volume":"101","author":"R Takemura","year":"2013","unstructured":"Takemura, R.: Proof theory for reasoning with Euler diagrams: a logic translation and normalization. Stud. Logica 101(1), 157\u2013191 (2013)","journal-title":"Stud. Logica"},{"key":"759_CR25","doi-asserted-by":"crossref","unstructured":"Takemura, R.: Towards a proof theory for heterogeneous logic combining sentences and diagrams. Diagrammatic Representation and Inference, Lecture Notes in Computer Science. Springer, pp. 607\u2013623 (2018)","DOI":"10.1007\/978-3-319-91376-6_55"},{"key":"759_CR26","doi-asserted-by":"crossref","unstructured":"Takemura, R., Shimojima, A., Katagiri, Y.: Logical investigation of reasoning with tables. Diagrammatic Representation and Inference, Lecture Notes in Computer Science, Springer 8578, 261\u2013276 (2014)","DOI":"10.1007\/978-3-662-44043-8_27"},{"key":"759_CR27","volume-title":"Autologic","author":"N Tennant","year":"1992","unstructured":"Tennant, N.: Autologic. Edinburgh University Press, Edinburgh (1992)"},{"key":"759_CR28","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"},{"key":"759_CR29","doi-asserted-by":"crossref","unstructured":"Urbas, M., Jamnik, M.: Heterogeneous Proofs: Spider diagrams meet higher-order provers. Interactive Theorem Proving, LNCS 6898, 376\u2013382 (2011)","DOI":"10.1007\/978-3-642-22863-6_29"},{"key":"759_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85108-0","volume-title":"Logic and Structure","author":"D van Dalen","year":"2004","unstructured":"van Dalen, D.: Logic and Structure, 4th edn. Springer, Berlin (2004)","edition":"4"},{"issue":"7","key":"759_CR31","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001530100091","volume":"40","author":"J von Plato","year":"2001","unstructured":"von Plato, J.: Natural deduction with general elimination rules. Arch. Math. Logic 40(7), 541\u2013567 (2001)","journal-title":"Arch. Math. Logic"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-020-00759-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-020-00759-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-020-00759-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,18]],"date-time":"2022-12-18T21:48:24Z","timestamp":1671400104000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-020-00759-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,24]]},"references-count":31,"journal-issue":{"issue":"7-8","published-print":{"date-parts":[[2021,11]]}},"alternative-id":["759"],"URL":"https:\/\/doi.org\/10.1007\/s00153-020-00759-y","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"type":"print","value":"0933-5846"},{"type":"electronic","value":"1432-0665"}],"subject":[],"published":{"date-parts":[[2021,2,24]]},"assertion":[{"value":"18 July 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 December 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 February 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}