{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T04:22:01Z","timestamp":1751516521177,"version":"3.41.0"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030783600"},{"type":"electronic","value":"9783030783617"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-78361-7_7","type":"book-chapter","created":{"date-parts":[[2021,7,3]],"date-time":"2021-07-03T00:48:50Z","timestamp":1625273330000},"page":"75-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Exploring Human-Computer Interaction in Mathematics: From Voevodsky\u2019s Univalent Foundations of Mathematics to\u00a0Mochizuki\u2019s IUT-Theoretic Proof of\u00a0the\u00a0ABC Conjecture"],"prefix":"10.1007","author":[{"given":"Yoshihiro","family":"Maruyama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,3]]},"reference":[{"key":"7_CR1","unstructured":"Abramsky, S.: Domain theory in logical form. In: Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science, pp. 47\u201353 (1987)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 415\u2013425 (2004)","DOI":"10.1109\/LICS.2004.1319636"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Temperley-Lieb Algebra: from Knot Theory to logic and computation via quantum mechanics. In: Mathematics of Quantum Computing and Quantum Technology, pp. 415\u2013458. Taylor & Francis (2008)","DOI":"10.1201\/9781584889007.ch15"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Brandenburger, A.: The sheaf-theoretic structure of non-locality and contextuality. New J. Phys. 13, 113036 (2011)","DOI":"10.1088\/1367-2630\/13\/11\/113036"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Hardy, L.: Logical Bell inequalities. Phys. Rev. A 85, 062114 (2012)","DOI":"10.1103\/PhysRevA.85.062114"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-642-41660-6_2","volume-title":"In Search of Elegance in the Theory and Practice of Computation","author":"S Abramsky","year":"2013","unstructured":"Abramsky, S.: Relational databases and Bell\u2019s Theorem. In: Tannen, V., Wong, L., Libkin, L., Fan, W., Tan, W.-C., Fourman, M. (eds.) In Search of Elegance in the Theory and Practice of Computation. LNCS, vol. 8000, pp. 13\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41660-6_2"},{"key":"7_CR7","unstructured":"Abramsky, S., et al.: Robust constraint satisfaction and local hidden variables in quantum mechanics. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, pp. 440\u2013446 (2013)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54789-8_1","volume-title":"Categories and Types in Logic, Language, and Physics","author":"S Abramsky","year":"2014","unstructured":"Abramsky, S., Sadrzadeh, M.: Semantic unification. In: Casadio, C., Coecke, B., Moortgat, M., Scott, P. (eds.) Categories and Types in Logic, Language, and Physics. LNCS, vol. 8222, pp. 1\u201313. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54789-8_1"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Intensionality definability and computation. Outstanding Contrib. Logic 5, 121\u2013142 (2014)","DOI":"10.1007\/978-3-319-06025-5_5"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Arrow\u2019s theorem by Arrow theory. In: Logic Without Borders: Essays on Set Theory, Model Theory, Philosophical Logic and Philosophy of Mathematics, pp. 15\u201330, de Gruyter (2015)","DOI":"10.1515\/9781614516873.15"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1017\/S0960129515000365","volume":"27","author":"S Abramsky","year":"2017","unstructured":"Abramsky, S., Winschel, V.: Coalgebraic analysis of subgame-perfect equilibria in infinite games without discounting. Math. Struct. Comput. Sci. 27, 751\u2013761 (2017)","journal-title":"Math. Struct. Comput. Sci."},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.inffus.2019.12.012","volume":"58","author":"AB Arrieta","year":"2020","unstructured":"Arrieta, A.B., et al.: Explainable Artificial Intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI. Inf. Fusion 58, 82\u2013115 (2020)","journal-title":"Inf. Fusion"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/philmat\/nkt030","volume":"22","author":"S Awodey","year":"2014","unstructured":"Awodey, S.: Structuralism, Invariance, and Univalence. Philosophia Math. 22, 1\u201311 (2014)","journal-title":"Philosophia Math."},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1017\/S0305004108001783","volume":"146","author":"S Awodey","year":"2009","unstructured":"Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. Camb. Phil. Soc. 146, 45\u201355 (2009)","journal-title":"Math. Proc. Camb. Phil. Soc."},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1080\/00029890.1950.11999523","volume":"4","author":"N Bourbaki","year":"1950","unstructured":"Bourbaki, N.: The architecture of mathematics. Am. Math. Mon. 4, 221\u2013232 (1950)","journal-title":"Am. Math. Mon."},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Castelvecchi, D.: Mathematical proof that rocked number theory will be published. Nature 580, 177 (2020). https:\/\/www.nature.com\/articles\/d41586-020-00998-2","DOI":"10.1038\/d41586-020-00998-2"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press (2013)","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"7_CR18","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1093\/analys\/58.1.7","volume":"58","author":"A Clark","year":"1998","unstructured":"Clark, A., Chalmers, D.: The extended mind. Analysis 58, 7\u201319 (1998)","journal-title":"Analysis"},{"key":"7_CR19","unstructured":"Coecke, B.: Automated quantum reasoning: non-logic - semi-logic - hyper-logic. In: Proceedings of AAAI Spring Symposium: Quantum Interaction, pp. 31\u201338 (2007)"},{"key":"7_CR20","first-page":"345","volume":"36","author":"B Coecke","year":"2010","unstructured":"Coecke, B., Sadrzadeh, M., Clark, S.: Mathematical foundations for a compositional distributional model of meaning. Linguist. Anal. 36, 345\u2013384 (2010)","journal-title":"Linguist. Anal."},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/11494645_12","volume-title":"New Computational Paradigms","author":"T Coquand","year":"2005","unstructured":"Coquand, T.: A logical approach to abstract algebra. In: Cooper, S.B., L\u00f6we, B., Torenvliet, L. (eds.) CiE 2005. LNCS, vol. 3526, pp. 86\u201395. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11494645_12"},{"key":"7_CR22","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.apal.2008.09.003","volume":"157","author":"T Coquand","year":"2009","unstructured":"Coquand, T.: Space of valuations. Ann. Pure Appl. Logic 157, 97\u2013109 (2009)","journal-title":"Ann. Pure Appl. Logic"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Streicher, T.: The groupoid interpretation of type theory, Twenty-five years of constructive type theory. Oxford Logic Guides, vol. 36, pp. 83\u2013111, Oxford University Press (1998)","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"7_CR24","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof \u2013 the four-color theorem. Not. AMS 55, 1382\u20131393 (2008)","journal-title":"Not. AMS"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Grothendieck, A., Dieudonne, J.: \u00c9l\u00e9ments de g\u00e9om\u00e9trie alg\u00e9brique. IHES (1960\u20131967)","DOI":"10.1007\/BF02684778"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Grothendieck, S A.: \u00e9minaire de G\u00e9om\u00e9trie Alg\u00e9brique du Bois Marie. IHES (1960\u20131967)","DOI":"10.1007\/BF02684778"},{"key":"7_CR27","unstructured":"von Hemholtz, H.: Vortr\u00e4ge und Reden, vol. 1, 4th edn. Vieweg und Sohn (1896)"},{"key":"7_CR28","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139171472","volume-title":"Proofs and Refutations","author":"I Lakatos","year":"1976","unstructured":"Lakatos, I.: Proofs and Refutations. Cambridge University Press, Cambridge (1976)"},{"key":"7_CR29","unstructured":"Loemker, J.: Leibniz: Philosophical Papers and Letters. D. Reidel, Synthese Historical Library (1969)"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Lurie, J.: Higher Topos Theory. Princeton University Press (2009)","DOI":"10.1515\/9781400830558"},{"key":"7_CR31","unstructured":"Lurie, J.: Higher Algebra (2017). https:\/\/www.math.ias.edu\/ lurie\/. Accessed 12 Feb 2021"},{"key":"7_CR32","unstructured":"Lurie, J.: Spectral Algebraic Geometry (2018). https:\/\/www.math.ias.edu\/ lurie\/. Accessed 12 Feb 2021"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Mancosu, P.: The Philosophy of Mathematical Practice. Oxford University Press (2008)","DOI":"10.1093\/acprof:oso\/9780199296453.001.0001"},{"key":"7_CR34","doi-asserted-by":"publisher","first-page":"1486","DOI":"10.1016\/j.apal.2010.05.002","volume":"161","author":"Y Maruyama","year":"2010","unstructured":"Maruyama, Y.: Fundamental results for Pointfree convex geometry. Ann. Pure Appl. Logic 161, 1486\u20131501 (2010)","journal-title":"Ann. Pure Appl. Logic"},{"key":"7_CR35","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1016\/j.jpaa.2011.07.002","volume":"216","author":"Y Maruyama","year":"2012","unstructured":"Maruyama, Y.: Natural duality, modality, and coalgebra. J. Pure Appl. Algebra 216, 565\u2013580 (2012)","journal-title":"J. Pure Appl. Algebra"},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-642-40206-7_17","volume-title":"Algebra and Coalgebra in Computer Science","author":"Y Maruyama","year":"2013","unstructured":"Maruyama, Y.: From operational Chu duality to Coalgebraic quantum symmetry. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 220\u2013235. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40206-7_17"},{"key":"7_CR37","unstructured":"Maruyama, Y.: Categorical Duality theory: with applications to domains, convexity, and the distribution monad. Leibniz Int. Proc. Inf. 23, 500\u2013520 (2013)"},{"key":"7_CR38","doi-asserted-by":"publisher","first-page":"3483","DOI":"10.1007\/s11229-015-0932-9","volume":"193","author":"Y Maruyama","year":"2016","unstructured":"Maruyama, Y.: Prior\u2019s Tonk, notions of logic, and levels of inconsistency: vindicating the Pluralistic Unity of Science in the light of categorical logical positivism. Synthese 193, 3483\u20133495 (2016)","journal-title":"Synthese"},{"key":"7_CR39","series-title":"Trends in Logic","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-319-22686-6_6","volume-title":"Advances in Proof-Theoretic Semantics","author":"Y Maruyama","year":"2016","unstructured":"Maruyama, Y.: Categorical harmony and paradoxes in\u00a0proof-theoretic semantics. In: Piecha, T., Schroeder-Heister, P. (eds.) Advances in Proof-Theoretic Semantics. TL, vol. 43, pp. 95\u2013114. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-22686-6_6"},{"key":"7_CR40","unstructured":"Maruyama, Y.: Meaning and duality: from categorical logic to quantum physics. D.Phil. thesis, University of Oxford (2017)"},{"key":"7_CR41","unstructured":"Maruyama, Y.: The dynamics of duality: a fresh look at the philosophy of duality. In: RIMS Kokyuroku (Proceedings of RIMS, Kyoto Univesity), vol. 2050, pp. 77\u201399 (2017)"},{"key":"7_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-34974-5_14","volume-title":"Modeling and Using Context","author":"Y Maruyama","year":"2019","unstructured":"Maruyama, Y.: Compositionality and contextuality: the symbolic and statistical theories of meaning. In: Bella, G., Bouquet, P. (eds.) CONTEXT 2019. LNCS (LNAI), vol. 11939, pp. 161\u2013174. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34974-5_14"},{"key":"7_CR43","series-title":"The Frontiers Collection","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-030-27569-3_15","volume-title":"WITTGENSTEINIAN (adj.)","author":"Y Maruyama","year":"2020","unstructured":"Maruyama, Y.: Foundations of mathematics: from Hilbert and Wittgenstein to the categorical unity of science. In: Wuppuluri, S., da Costa, N. (eds.) WITTGENSTEINIAN (adj.). TFC, pp. 245\u2013274. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-27569-3_15"},{"key":"7_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-030-52152-3_25","volume-title":"Artificial General Intelligence","author":"Y Maruyama","year":"2020","unstructured":"Maruyama, Y.: The conditions of artificial general intelligence: logic, autonomy, resilience, integrity, morality, emotion, embodiment, and embeddedness. In: Goertzel, B., Panov, A.I., Potapov, A., Yampolskiy, R. (eds.) AGI 2020. LNCS (LNAI), vol. 12177, pp. 242\u2013251. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-52152-3_25"},{"key":"7_CR45","doi-asserted-by":"publisher","first-page":"2616","DOI":"10.1080\/00927872.2020.1721520","volume":"48","author":"Y Maruyama","year":"2020","unstructured":"Maruyama, Y.: Topological duality via maximal spectrum functor. Comm. Algebra 48, 2616\u20132623 (2020)","journal-title":"Comm. Algebra"},{"key":"7_CR46","doi-asserted-by":"crossref","unstructured":"Maruyama, Y.: Universal stone duality via the concept of topological dualizability and its applications to many-valued logic. In: Proceedings of FUZZ-IEEE. IEEE Computer Society (2020)","DOI":"10.1109\/FUZZ48607.2020.9177848"},{"key":"7_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-030-67220-1_11","volume-title":"Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops","author":"Y Maruyama","year":"2021","unstructured":"Maruyama, Y.: Symbolic and statistical theories of cognition: towards integrated artificial intelligence. In: Cleophas, L., Massink, M. (eds.) SEFM 2020. LNCS, vol. 12524, pp. 129\u2013146. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67220-1_11"},{"key":"7_CR48","unstructured":"Maruyama, Y.: Duality, Intensionality, and Contextuality, accepted for publication in a volume of Outstanding Contributions to Logic. Springer (2021)"},{"key":"7_CR49","unstructured":"Mochizuki, S.: Inter-Universal Teichmuller Theory I-IV (2012). http:\/\/www.kurims.kyoto-u.ac.jp\/ motizuki\/. Accessed 12 Feb 2021"},{"key":"7_CR50","doi-asserted-by":"crossref","unstructured":"Reichenbach, H.: Selected Writings: 1909\u20131953, Reidel (1978)","DOI":"10.1007\/978-94-009-9855-1"},{"key":"7_CR51","doi-asserted-by":"publisher","first-page":"524","DOI":"10.2307\/2026089","volume":"78","author":"W Tait","year":"1981","unstructured":"Tait, W.: Finitism. J. Philos. 78, 524\u2013546 (1981)","journal-title":"J. Philos."},{"key":"7_CR52","unstructured":"Terui, K.: A flaw in R.B. White\u2019s article \u201cThe consistency of the axiom of comprehension in the infinite-valued predicate logic of \u0141ukasiewicz\u201d (2014). http:\/\/www.kurims.kyoto-u.ac.jp\/ terui\/whitenew.pdf. Accessed 12 Feb 2020"},{"key":"7_CR53","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1090\/S0273-0979-1994-00502-6","volume":"30","author":"WP Thurston","year":"1994","unstructured":"Thurston, W.P.: On proof and progress in mathematics. Bull. AMS 30, 161\u2013177 (1994)","journal-title":"Bull. AMS"},{"key":"7_CR54","unstructured":"Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Princeton IAS (2013)"},{"key":"7_CR55","unstructured":"Voevodsky, V.: The Origins and Motivations of Univalent Foundations, Princeton IAS (2014). https:\/\/www.ias.edu\/ideas\/2014\/voevodsky-origins. Accessed 10 Feb 2021"},{"key":"7_CR56","unstructured":"Weingart, P.: A short history of knowledge formations. In: The Oxford Handbook of Interdisciplinarity, pp. 3\u201314. Oxford University Press (2010)"},{"key":"7_CR57","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/BF00258447","volume":"8","author":"RB White","year":"1979","unstructured":"White, R.B.: The consistency of the axiom of comprehension in the infinite-valued predicate logic of \u0141ukasiewicz. J. Philos. Log. 8, 509\u2013534 (1979)","journal-title":"J. Philos. Log."}],"container-title":["Lecture Notes in Computer Science","Human Interface and the Management of Information. Information-Rich and Intelligent Environments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-78361-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T22:27:06Z","timestamp":1751495226000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-78361-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030783600","9783030783617"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-78361-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"3 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"HCII","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Human-Computer Interaction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"hcii2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/2021.hci.international\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}