{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T18:59:34Z","timestamp":1782327574228,"version":"3.54.5"},"reference-count":108,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T00:00:00Z","timestamp":1747699200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T00:00:00Z","timestamp":1747699200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R006865\/1"],"award-info":[{"award-number":["EP\/R006865\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/S013008\/1"],"award-info":[{"award-number":["EP\/S013008\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Topoi"],"published-print":{"date-parts":[[2026,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    The development of logic has largely been through the\n                    <jats:italic>deductive<\/jats:italic>\n                    paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual\n                    <jats:italic>reductive<\/jats:italic>\n                    perspective: collections of sufficient premisses are generated from putative conclusions. We call this paradigm,\n                    <jats:italic>reductive logic<\/jats:italic>\n                    . This expression of logic encompass as diverse reasoning activities as proving a formula in a formal system to seeking to meet a friend before noon on Saturday. This paper is a semantical analysis of reductive logic. In particular, we provide mathematical foundations for representing and reasoning about\n                    <jats:italic>reduction operators<\/jats:italic>\n                    . Heuristically, reduction operators may be thought of as \u2018backwards\u2019 inference rules. In this paper, we address their mathematical representation, how they are used in the context of reductive reasoning, and, crucially, what makes them\n                    <jats:italic>valid<\/jats:italic>\n                    .\n                  <\/jats:p>","DOI":"10.1007\/s11245-025-10211-6","type":"journal-article","created":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T10:54:04Z","timestamp":1747738444000},"page":"675-691","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Semantic Foundations of Reductive Reasoning"],"prefix":"10.1007","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7144-6910","authenticated-orcid":false,"given":"Alexander V.","family":"Gheorghiu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David J.","family":"Pym","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,20]]},"reference":[{"key":"10211_CR1","unstructured":"van Atten M (2022) The Development of Intuitionistic Logic. The Stanford Encyclopedia of Philosophy"},{"issue":"2","key":"10211_CR2","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H Barendregt","year":"1991","unstructured":"Barendregt H (1991) Introduction to Generalized Type Systems. Journal of Functional Programming 1(2):125\u2013154","journal-title":"Journal of Functional Programming"},{"key":"10211_CR3","doi-asserted-by":"crossref","unstructured":"Barendregt H, Dekkers W, Statman R (2013) Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press","DOI":"10.1017\/CBO9781139032636"},{"key":"10211_CR4","first-page":"117","volume-title":"Lambda calculi with types","author":"HP Barendregt","year":"1993","unstructured":"Barendregt HP (1993) Lambda calculi with types. Oxford University Press Inc, USA, pp 117\u2013309"},{"key":"10211_CR5","unstructured":"Barwise J, Moss L (1996) Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena. Cambridge University Press"},{"key":"10211_CR6","volume-title":"The Stanford Encyclopedia of Philosophy, Fall","author":"M Beaney","year":"2024","unstructured":"Beaney M, Raysmith T (2024) Analysis. In: Zalta EN, Nodelman U (eds) The Stanford Encyclopedia of Philosophy, Fall, 2024th edn. Stanford University, Metaphysics Research Lab","edition":"2024"},{"key":"10211_CR7","doi-asserted-by":"crossref","unstructured":"Bergstra JA, Klop JW (1984) The algebra of recursively defined processes and the algebra of regular processes. International Colloquium on Automata, Languages, and Programming pp 82\u201394","DOI":"10.1007\/3-540-13345-3_7"},{"key":"10211_CR8","doi-asserted-by":"publisher","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive Theorem Proving and Program Development. Springer. https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"4","key":"10211_CR9","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1016\/S1385-7258(55)50014-6","volume":"17","author":"EW Beth","year":"1955","unstructured":"Beth EW (1955) Semantic Construction of Intuitionistic Logic. Indagationes Mathematicae 17(4):327\u2013338. https:\/\/doi.org\/10.1016\/S1385-7258(55)50014-6","journal-title":"Indagationes Mathematicae"},{"issue":"1","key":"10211_CR10","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/200836.200876","volume":"42","author":"B Bloom","year":"1995","unstructured":"Bloom B, Istrail S, Meyer AR (1995) Bisimulation can\u2019t be traced. Journal of the ACM 42(1):232\u2013268","journal-title":"Journal of the ACM"},{"key":"10211_CR11","doi-asserted-by":"publisher","unstructured":"Bonchi F, Zanasi F (2015) Bialgebraic Semantics for Logic Programming. Logical Methods in Computer Science 11(1). https:\/\/doi.org\/10.2168\/LMCS-11(1:14)2015","DOI":"10.2168\/LMCS-11(1:14)2015"},{"key":"10211_CR12","doi-asserted-by":"crossref","unstructured":"Brandom R (2000) Articulating Reasons: An Introduction to Inferentialism. Harvard University Press","DOI":"10.4159\/9780674028739"},{"issue":"2","key":"10211_CR13","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1090\/S0002-9904-1913-02440-6","volume":"20","author":"LEJ Brouwer","year":"1913","unstructured":"Brouwer LEJ (1913) Intuitionism and Formalism. Bulletin of the American Mathematical Society 20(2):81\u201396","journal-title":"Bulletin of the American Mathematical Society"},{"key":"10211_CR14","unstructured":"Bundy A (1985) The Computer Modelling of Mathematical Reasoning. Academic Press Professional, Inc"},{"key":"10211_CR15","volume-title":"Proof planning","author":"A Bundy","year":"1998","unstructured":"Bundy A (1998) Proof planning. University of Edinburgh, Department of Artificial Intelligence, Tech. rep"},{"key":"10211_CR16","unstructured":"Cartmell J (1978) Generalised Algebraic Theories and Contextual Categories. PhD thesis, Oxford University"},{"key":"10211_CR17","doi-asserted-by":"crossref","unstructured":"Cheng E (2022) The Joy of Abstraction. An exploration of math, category theory, and life. Cambridge University Press","DOI":"10.1017\/9781108769389"},{"key":"10211_CR18","doi-asserted-by":"crossref","unstructured":"Clark KL (1977) Negation as Failure. Logic and Data Bases pp 293\u2013322","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"10211_CR19","unstructured":"Coq Team (2024) The Coq Proof Assistant. https:\/\/coq.inria.fr\/. Accessed July 2024"},{"key":"10211_CR20","volume-title":"Logic and Structure","author":"D van Dalen","year":"2012","unstructured":"van Dalen D (2012) Logic and Structure. Universitext, Springer"},{"key":"10211_CR21","doi-asserted-by":"crossref","unstructured":"Eckhardt T, Pym DJ (2024) Proof-theoretic Semantics for Modal Logics. Logic Journal of the IGPL In Press - arXiv:2401.13597","DOI":"10.1093\/jigpal\/jzae004"},{"key":"10211_CR22","doi-asserted-by":"publisher","unstructured":"Farooque M, Graham-Lengrand S, Mahboubi A (2013) A Bisimulation between DPLL(T) and a Proof-search Strategy for the Focused Sequent Calculus, Association for Computing Machinery, p 3-14. https:\/\/doi.org\/10.1145\/2503887.2503892","DOI":"10.1145\/2503887.2503892"},{"key":"10211_CR23","unstructured":"Fitch FB (1952) Symbolic Logic: An Introduction. Ronald Press Co"},{"key":"10211_CR24","unstructured":"Francez N (2015) Proof-theoretic Semantics. College Publications"},{"key":"10211_CR25","unstructured":"Frank Pfenning, Carsten Sch\u00fcrmann, Brigitte Pientka, Roberta Vigo, and Kevin Watkins (2024) The Twelf Project. http:\/\/twelf.org\/wiki\/Main_Page. Accessed July 2024"},{"key":"10211_CR26","unstructured":"Friedman H (1975) Some systems of second order arithmetic and their use. In: Proceedings of the International Congress of Mathematicians, vol\u00a01. Canadian Mathematical Congress, pp 235\u2013242"},{"key":"10211_CR27","unstructured":"Gheorghiu A, Pym DJ (2023a) Proof-theoretic Semantics and Tactical Proof. arXiv:2301.02302 Accessed July 2024"},{"key":"10211_CR28","doi-asserted-by":"publisher","unstructured":"Gheorghiu AV, Pym DJ (2023) Defining Logical Systems via Algebraic Constraints on Proofs. Journal of Logic and Computation. https:\/\/doi.org\/10.1093\/logcom\/exad065","DOI":"10.1093\/logcom\/exad065"},{"issue":"4","key":"10211_CR29","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1007\/s11225-022-10028-z","volume":"111","author":"AV Gheorghiu","year":"2023","unstructured":"Gheorghiu AV, Pym DJ (2023) Semantical Analysis of the Logic of Bunched Implications. Studia Logica 111(4):525\u2013571","journal-title":"Studia Logica"},{"key":"10211_CR30","doi-asserted-by":"crossref","unstructured":"Gheorghiu AV, Docherty S, Pym DJ (2023a) Reductive Logic, Proof-Search, and Coalgebra: A Perspective from Resource Semantics. Samson Abramsky on Logic and Structure in Computer Science and Beyond pp 833\u2013875","DOI":"10.1007\/978-3-031-24117-8_23"},{"key":"10211_CR31","doi-asserted-by":"crossref","unstructured":"Gheorghiu AV, Gu T, Pym. DJ (2023b) Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic. In: Automated Reasoning with Analytic Tableaux and Related Methods \u2014 TABLEAUX. Springer, pp 367\u2013385","DOI":"10.1007\/978-3-031-43513-3_20"},{"key":"10211_CR32","unstructured":"Gheorghiu AV, Gu T, Pym DJ (2024) A Note on the Practice of Logical Inferentialism. In: 2nd Logic and Philosophy conference, in Press \u2014 arXiv:2403.10546"},{"key":"10211_CR33","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198751588.001.0001","volume-title":"Artificial Intelligence and Scientific Method","author":"D Gillies","year":"1996","unstructured":"Gillies D (1996) Artificial Intelligence and Scientific Method. Oxford University Press"},{"issue":"1","key":"10211_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard JY (1987) Linear Logic. Theoretical Computer Science 50(1):1\u2013101","journal-title":"Theoretical Computer Science"},{"key":"10211_CR35","volume-title":"Introduction to HOL","author":"MJ Gordon","year":"1993","unstructured":"Gordon MJ, Melham TF (1993) Introduction to HOL. Cambridge University Press, A theorem proving environment for higher order logic"},{"key":"10211_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"MJ Gordon","year":"1979","unstructured":"Gordon MJ, Wadsworth CP, Milner R (1979) Edinburgh LCF. Springer, A mechanised logic of computation. https:\/\/doi.org\/10.1007\/3-540-09724-4"},{"key":"10211_CR37","doi-asserted-by":"crossref","unstructured":"Gordon MJC (2015) Tactics for mechanized reasoning: a commentary on milner (1984)\u2018the use of machines to assist in rigorous proof\u2019. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 373(2039)","DOI":"10.1098\/rsta.2014.0234"},{"key":"10211_CR38","doi-asserted-by":"crossref","unstructured":"Gu T, Gheorghiu AV, Pym DJ (2023) Proof-theoretic Semantics for the Logic of Bunched Implications. arXiv:2311.16719 Accessed February 2024","DOI":"10.1007\/s11225-025-10202-z"},{"key":"10211_CR39","doi-asserted-by":"crossref","unstructured":"Gupta G, Bansal A, Min R, et\u00a0al. (2007) Coinductive Logic Programming and its Applications. In: International Conference Logic Programming \u2014 ICLP. Springer, pp 27\u201344","DOI":"10.1007\/978-3-540-74610-2_4"},{"key":"10211_CR40","doi-asserted-by":"crossref","unstructured":"Harland J, Pym DJ (1997) Resource-distribution via Boolean Constraints. In: Automated Deduction \u2014 CADE. Springer, pp 222\u2013236","DOI":"10.1007\/3-540-63104-6_21"},{"issue":"1","key":"10211_CR41","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/601775.601778","volume":"4","author":"J Harland","year":"2003","unstructured":"Harland J, Pym DJ (2003) Resource-distribution via Boolean Constraints. ACM Transactions on Computational Logic 4(1):56\u201390","journal-title":"ACM Transactions on Computational Logic"},{"key":"10211_CR42","unstructured":"Heyting A (1989) Intuitionism: An Introduction. Cambridge University Press"},{"issue":"2","key":"10211_CR43","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"JS Hodas","year":"1994","unstructured":"Hodas JS, Miller D (1994) Logic Programming in a Fragment of Intuitionistic Linear Logic. Information and Computation 110(2):327\u2013365","journal-title":"Information and Computation"},{"key":"10211_CR44","doi-asserted-by":"publisher","unstructured":"Hofmann M (1997) Syntax and Semantics of Dependent Types. Semantics and Logics of Computation p 79-130. https:\/\/doi.org\/10.1017\/CBO9780511526619.004","DOI":"10.1017\/CBO9780511526619.004"},{"key":"10211_CR45","first-page":"479","volume":"44","author":"WA Howard","year":"1980","unstructured":"Howard WA (1980) The Formulae-as-Types Notion of Construction. To H B Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism 44:479\u2013490","journal-title":"To H B Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism"},{"key":"10211_CR46","unstructured":"Jacobs B (1991) Categorical Type Theory. PhD thesis, The University of Nijmegen"},{"key":"10211_CR47","volume-title":"Introduction to Coalgebra,","author":"B Jacobs","year":"2017","unstructured":"Jacobs B (2017) Introduction to Coalgebra, vol 59. Cambridge University Press"},{"key":"10211_CR48","volume-title":"Mathematical Logic","author":"SC Kleene","year":"1961","unstructured":"Kleene SC (1961) Mathematical Logic. Wiley and Sons"},{"key":"10211_CR49","first-page":"133","volume":"6","author":"B Knaster","year":"1928","unstructured":"Knaster B, Tarksi A (1928) Un Th\u00e9or\u00e8me sur les Fonctions d\u2019Ensembles. Annales de la Societe Polonaise de Mathematique 6:133\u2013134","journal-title":"Annales de la Societe Polonaise de Mathematique"},{"key":"10211_CR50","doi-asserted-by":"crossref","unstructured":"Kolmogorov A (1932) Zur Deutung der Intuitionistischen Logik. Mathematische Zeitschift 35","DOI":"10.1007\/BF01186549"},{"key":"10211_CR51","doi-asserted-by":"crossref","unstructured":"Komendantskaya E, Power J (2011) Coalgebraic Semantics for Derivations in Logic Programming. International Conference on Algebra and Coalgebra in Computer Science pp 268\u2013282","DOI":"10.1007\/978-3-642-22944-2_19"},{"key":"10211_CR52","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-642-17796-5_7","volume":"13","author":"E Komendantskaya","year":"2011","unstructured":"Komendantskaya E, McCusker G, Power J (2011) Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming. International Conference on Algebraic Methodology and Software Technology - AMAST 13:111\u2013127","journal-title":"International Conference on Algebraic Methodology and Software Technology - AMAST"},{"issue":"2","key":"10211_CR53","doi-asserted-by":"crossref","first-page":"745","DOI":"10.1093\/logcom\/exu026","volume":"26","author":"E Komendantskaya","year":"2016","unstructured":"Komendantskaya E, Power J, Schmidt M (2016) Coalgebraic Logic Programming: from Semantics to Implementation. Journal of Logic and Computation 26(2):745\u2013783","journal-title":"Journal of Logic and Computation"},{"issue":"7","key":"10211_CR54","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1145\/359131.359136","volume":"22","author":"R Kowalski","year":"1979","unstructured":"Kowalski R (1979) Algorithm = Logic + Control. Communications of the ACM 22(7):424\u2013436","journal-title":"Communications of the ACM"},{"key":"10211_CR55","unstructured":"Kowalski R (1986) Logic for Problem-Solving. North-Holland Publishing Co"},{"issue":"3","key":"10211_CR56","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R Kowalski","year":"1971","unstructured":"Kowalski R, Kuehner D (1971) Linear resolution with selection function. Artificial Intelligence 2(3):227\u2013260. https:\/\/doi.org\/10.1016\/0004-3702(71)90012-9","journal-title":"Artificial Intelligence"},{"key":"10211_CR57","doi-asserted-by":"crossref","unstructured":"Kripke SA (1965) Semantical Analysis of Intuitionistic Logic I, vol\u00a040, Elsevier, pp 92\u2013130","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"10211_CR58","first-page":"375","volume-title":"From $$\\lambda $$-calculus to Cartesian Closed Categories","author":"J Lambek","year":"1980","unstructured":"Lambek J (1980) From $$\\lambda $$-calculus to Cartesian Closed Categories. Essays on Combinatory Logic, Lambda Calculus and Formalism, To H B Curry, pp 375\u2013402"},{"key":"10211_CR59","unstructured":"Lemmon EJ (1978) Beginning Logic. Hackett Publishing"},{"issue":"1","key":"10211_CR60","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1093\/jigpal\/jzt038","volume":"22","author":"D Makinson","year":"2014","unstructured":"Makinson D (2014) On an Inferential Semantics for Classical Logic. Logic Journal of IGPL 22(1):147\u2013154","journal-title":"Logic Journal of IGPL"},{"key":"10211_CR61","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/S0049-237X(08)71945-1","volume":"80","author":"P Martin-L\u00f6f","year":"1975","unstructured":"Martin-L\u00f6f P (1975) An Intuitionistic Theory of Types: Predicative Part. Studies in Logic and the Foundations of Mathematics 80:73\u2013118","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"issue":"1\u20132","key":"10211_CR62","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0743-1066(89)90031-9","volume":"6","author":"D Miller","year":"1989","unstructured":"Miller D (1989) A Logical Analysis of Modules in Logic Programming. The Journal of Logic Programming 6(1\u20132):79\u2013108","journal-title":"The Journal of Logic Programming"},{"issue":"1\u20132","key":"10211_CR63","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D Miller","year":"1991","unstructured":"Miller D, Nadathur G, Pfenning F et al (1991) Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied logic 51(1\u20132):125\u2013157","journal-title":"Annals of Pure and Applied logic"},{"issue":"3","key":"10211_CR64","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R Milner","year":"1983","unstructured":"Milner R (1983) Calculi for Synchrony and Asynchrony. Theoretical Computer Science 25(3):267\u2013310","journal-title":"Theoretical Computer Science"},{"issue":"1522","key":"10211_CR65","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1098\/rsta.1984.0067","volume":"312","author":"R Milner","year":"1984","unstructured":"Milner R (1984) The Use of Machines to Assist in Rigorous Proof. Philosophical Transactions of the Royal Society of London Series A, Mathematical and Physical Sciences 312(1522):411\u2013422","journal-title":"Philosophical Transactions of the Royal Society of London Series A, Mathematical and Physical Sciences"},{"key":"10211_CR66","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner R (1989) Communication and Concurrency. Prentice Hall"},{"key":"10211_CR67","unstructured":"Nascimento V (2023) Foundational studies in proof-theoretic semantics. PhD thesis, Universidade do Estado do Rio de Janeiro"},{"key":"10211_CR68","unstructured":"Nascimento V, Pereira LC, Pimentel E (2023) An Ecumenical view of Proof-theoretic Semantics. arXiv:2306.03656 Accessed July 2024"},{"issue":"5","key":"10211_CR69","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","volume":"34","author":"S Negri","year":"2005","unstructured":"Negri S (2005) Proof Analysis in Modal Logic. Journal of Philosophical Logic 34(5):507\u2013544","journal-title":"Journal of Philosophical Logic"},{"key":"10211_CR70","unstructured":"nLab (2021) free functor. https:\/\/ncatlab.org\/nlab\/show\/free+functor. Accessed July 2024"},{"issue":"2","key":"10211_CR71","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"PW O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn PW, Pym DJ (1999) The Logic of Bunched Implications. Bulletin of Symbolic Logic 5(2):215\u2013244","journal-title":"Bulletin of Symbolic Logic"},{"key":"10211_CR72","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","author":"LC Paulson","year":"1994","unstructured":"Paulson LC (1994) Isabelle: A Generic Theorem Prover. Springer. https:\/\/doi.org\/10.1007\/BFb0030541","journal-title":"Springer"},{"key":"10211_CR73","unstructured":"Pavlovi\u0107 D (1990) Predicates and Fibrations. PhD thesis, University of Utrecht"},{"key":"10211_CR74","doi-asserted-by":"crossref","unstructured":"Pfenning F, Sch\u00fcrmann C (1999) System description: Twelf \u2014 a meta-logical framework for deductive systems. In: Automated Deduction \u2014 CADE, pp 202\u2013206","DOI":"10.1007\/3-540-48660-7_14"},{"key":"10211_CR75","doi-asserted-by":"crossref","unstructured":"Piecha T (2016) Completeness in Proof-theoretic Semantics. Advances in Proof-theoretic Semantics pp 231\u2013251","DOI":"10.1007\/978-3-319-22686-6_15"},{"issue":"1","key":"10211_CR76","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/s11225-018-9823-7","volume":"107","author":"T Piecha","year":"2019","unstructured":"Piecha T, Schroeder-Heister P (2019) Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-theoretic Semantics. Studia Logica 107(1):233\u2013246","journal-title":"Studia Logica"},{"issue":"3","key":"10211_CR77","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/s10992-014-9322-x","volume":"44","author":"T Piecha","year":"2015","unstructured":"Piecha T, de Campos Sanz W, Schroeder-Heister P (2015) Failure of Completeness in Proof-theoretic Semantics. Journal of Philosophical Logic 44(3):321\u2013335","journal-title":"Journal of Philosophical Logic"},{"key":"10211_CR78","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-93862-6","volume-title":"The Efficiency of Theorem Proving Strategies","author":"DA Plaisted","year":"1997","unstructured":"Plaisted DA, Zhu Y (1997) The Efficiency of Theorem Proving Strategies. Springer"},{"key":"10211_CR79","volume-title":"A Structural approach to Operational Semantics","author":"GD Plotkin","year":"1981","unstructured":"Plotkin GD (1981) A Structural approach to Operational Semantics. Aarhus University, Tech. rep"},{"key":"10211_CR80","unstructured":"Portoraro F (2024) Automated Reasoning. In: Zalta EN, Nodelman U (eds) The Stanford Encyclopedia of Philosophy, Spring, 2024th edn. Stanford University, Metaphysics Research Lab"},{"key":"10211_CR81","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198526339.001.0001","volume-title":"Reductive Logic and Proof-search: Proof Theory, Semantics, and Control, Oxford Logic Guides,","author":"DJ Pym","year":"2004","unstructured":"Pym DJ, Ritter E (2004) Reductive Logic and Proof-search: Proof Theory, Semantics, and Control, Oxford Logic Guides, vol 45. Oxford University Press"},{"key":"10211_CR82","doi-asserted-by":"crossref","unstructured":"Pym DJ, Wallen LA (1993) Logic programming via proof-valued computations. In: Proceedings of the UK Conference on Logic Programming \u2014 ALPUK. Springer, pp 253\u2013262","DOI":"10.1007\/978-1-4471-3421-3_14"},{"key":"10211_CR83","doi-asserted-by":"publisher","unstructured":"Pym DJ, Ritter E, Robinson E (2024) Categorical proof-theoretic semantics. Studia Logica pp 1\u201338. https:\/\/doi.org\/10.1007\/s11225-024-10101-9","DOI":"10.1007\/s11225-024-10101-9"},{"key":"10211_CR84","unstructured":"Reitzig R (2012) Discussion on Computer Science Stack Exchange. https:\/\/cs.stackexchange.com\/questions\/525\/what-is-coinduction. Accessed June 2024"},{"issue":"1","key":"10211_CR85","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J Rutten","year":"2000","unstructured":"Rutten J (2000) Universal Coalgebra: a theory of systems. Theoretical Computer Science 249(1):3\u201380. https:\/\/doi.org\/10.1016\/S0304-3975(00)00056-6","journal-title":"Theoretical Computer Science"},{"key":"10211_CR86","unstructured":"Sandqvist T (2005) An inferentialist Interpretation of Classical Logic. PhD thesis, Uppsala University"},{"issue":"2","key":"10211_CR87","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1093\/analys\/anp003","volume":"69","author":"T Sandqvist","year":"2009","unstructured":"Sandqvist T (2009) Classical logic without Bivalence. Analysis 69(2):211\u2013218","journal-title":"Analysis"},{"issue":"5","key":"10211_CR88","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1093\/jigpal\/jzv021","volume":"23","author":"T Sandqvist","year":"2015","unstructured":"Sandqvist T (2015) Base-extension Semantics for Intuitionistic Sentential Logic. Logic Journal of the IGPL 23(5):719\u2013731","journal-title":"Logic Journal of the IGPL"},{"key":"10211_CR89","volume-title":"Categories for the Working Mathematician","author":"Saunders MacLane","year":"1971","unstructured":"MacLane Saunders (1971) Categories for the Working Mathematician. Springer"},{"issue":"4","key":"10211_CR90","doi-asserted-by":"crossref","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"P Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister P (1984) A natural extension of natural deduction. The Journal of Symbolic Logic 49(4):1284\u20131300","journal-title":"The Journal of Symbolic Logic"},{"issue":"3","key":"10211_CR91","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1007\/s11229-004-6296-1","volume":"148","author":"P Schroeder-Heister","year":"2006","unstructured":"Schroeder-Heister P (2006) Validity Concepts in Proof-theoretic Semantics. Synthese 148(3):525\u2013571","journal-title":"Synthese"},{"key":"10211_CR92","unstructured":"Schroeder-Heister P (2008) Proof-Theoretic versus Model-Theoretic Consequence. The Logica Yearbook 2007"},{"key":"10211_CR93","unstructured":"Schroeder-Heister P (2018) Proof-theoretic Semantics. The Stanford Encyclopedia of Philosophy"},{"key":"10211_CR94","doi-asserted-by":"crossref","unstructured":"Seely RA (1983) Hyperdoctrines, Natural Deduction and the Beck condition. Mathematical Logic Quarterly 29(10):505\u2013542","DOI":"10.1002\/malq.19830291005"},{"key":"10211_CR95","doi-asserted-by":"crossref","unstructured":"Simon L, Bansal A, Mallya A, et\u00a0al. (2007) Co-Logic Programming: extending logic programming with coinduction. In: International Colloquium on Automata, Languages and Programming \u2014 ICALP. Springer, pp 472\u2013483","DOI":"10.1007\/978-3-540-73420-8_42"},{"key":"10211_CR96","doi-asserted-by":"publisher","unstructured":"Smullyan RM (1968) Analytic Tableaux, Springer, pp 15\u201330. https:\/\/doi.org\/10.1007\/978-3-642-86718-7_2","DOI":"10.1007\/978-3-642-86718-7_2"},{"key":"10211_CR97","doi-asserted-by":"crossref","unstructured":"Stafford W (2021) Proof-theoretic Semantics and Inquisitive Logic. Journal of Philosophical Logic","DOI":"10.1007\/s10992-021-09596-7"},{"key":"10211_CR98","doi-asserted-by":"publisher","unstructured":"Stafford W, Nascimento V (2023) Following all the Rules: Intuitionistic Completeness for Generalized Proof-theoretic Validity. Analysis. https:\/\/doi.org\/10.1093\/analys\/anac100","DOI":"10.1093\/analys\/anac100"},{"key":"10211_CR99","unstructured":"Streicher T (1988) Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions. PhD thesis, University of Passau"},{"key":"10211_CR100","unstructured":"Szabo ME (ed) (1969) The Collected Papers of Gerhard Gentzen. North-Holland Publishing Company"},{"key":"10211_CR101","unstructured":"Tarski A (1936) On the Concept of Logical Consequence. Logic, semantics, metamathematics 52:409\u2013420"},{"issue":"2","key":"10211_CR102","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski A (1955) A Lattice-theoretical Fixpoint Theorem and Its Applications. Pacific Journal of Mathematics 5(2):285\u2013309","journal-title":"Pacific Journal of Mathematics"},{"key":"10211_CR103","volume-title":"Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science,","author":"AS Troelstra","year":"2000","unstructured":"Troelstra AS, Schwichtenberg H (2000) Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, vol 43. Cambridge University Press"},{"key":"10211_CR104","doi-asserted-by":"publisher","unstructured":"Turi D, Plotkin GD (1997) Towards a Mathematical Operational Semantics. In: Logic in Computer Science \u2014 LICS. IEEE, pp 280\u2013291, https:\/\/doi.org\/10.1109\/LICS.1997.614955","DOI":"10.1109\/LICS.1997.614955"},{"key":"10211_CR105","unstructured":"Wallen LA (1987) Automated proof search in non-classical logics : efficient matrix proof methods for modal and intuitionistic logics. PhD thesis, University of Edinburgh"},{"key":"10211_CR106","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1023\/A:1005217827758","volume":"64","author":"H Wansing","year":"2000","unstructured":"Wansing H (2000) The Idea of a Proof-theoretic Semantics and the Meaning of the Logical Operations. Studia Logica 64:3\u201320","journal-title":"Studia Logica"},{"key":"10211_CR107","unstructured":"Wikipedia Proof Assistant. https:\/\/en.wikipedia.org\/wiki\/Proof_assistant"},{"issue":"1","key":"10211_CR108","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/j.tcs.2004.12.009","volume":"338","author":"J Worrell","year":"2005","unstructured":"Worrell J (2005) On the Final Sequence of a Finitary Set Functor. Theoretical Computer Science 338(1):184\u2013199. https:\/\/doi.org\/10.1016\/j.tcs.2004.12.009","journal-title":"Theoretical Computer Science"}],"container-title":["Topoi"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11245-025-10211-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11245-025-10211-6","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11245-025-10211-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T15:42:22Z","timestamp":1780674142000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11245-025-10211-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,20]]},"references-count":108,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,5]]}},"alternative-id":["10211"],"URL":"https:\/\/doi.org\/10.1007\/s11245-025-10211-6","relation":{},"ISSN":["0167-7411","1572-8749"],"issn-type":[{"value":"0167-7411","type":"print"},{"value":"1572-8749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,20]]},"assertion":[{"value":"17 April 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 May 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no conflict of interest to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}