{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T18:51:58Z","timestamp":1780599118357,"version":"3.54.1"},"reference-count":71,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T00:00:00Z","timestamp":1701043200000},"content-version":"vor","delay-in-days":3,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,1,17]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; e.g. one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of decomposition is to obtain a tool for uniform and modular treatment of proof theory and to provide a bridge between semantics logics and their proof theory. The paper discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics: including, a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic.<\/jats:p>","DOI":"10.1093\/logcom\/exad065","type":"journal-article","created":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T23:27:21Z","timestamp":1701127641000},"page":"95-146","source":"Crossref","is-referenced-by-count":2,"title":["Defining logical systems via algebraic constraints on proofs"],"prefix":"10.1093","volume":"35","author":[{"given":"Alexander V","family":"Gheorghiu","sequence":"first","affiliation":[{"name":"University College London , London WC1E 6BT, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David J","family":"Pym","sequence":"additional","affiliation":[{"name":"University College London , London WC1E 6BT, UK"},{"name":"Institute of Philosophy, University of London , London WC1H 0AR, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"286","published-online":{"date-parts":[[2023,11,24]]},"reference":[{"key":"2025011715020773900_ref1","volume-title":"Normal Multimodal Logics: Automatic Deduction and Logic Programming Extension","author":"Baldoni","year":"1998"},{"key":"2025011715020773900_ref2","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1023\/A:1005003904639","article-title":"Natural deduction for non-classical logics","volume":"60","author":"Basin","year":"1998","journal-title":"Studia Logica"},{"key":"2025011715020773900_ref3","first-page":"327","article-title":"Semantic construction of intuitionistic logic","volume":"17","author":"Beth","year":"1955","journal-title":"Indagationes Mathematicae"},{"key":"2025011715020773900_ref4","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1093\/logcom\/10.1.137","article-title":"Internalizing labelled deduction","volume":"10","author":"Blackburn","year":"2000","journal-title":"Journal of Logic and Computation"},{"key":"2025011715020773900_ref5","volume-title":"Modal Logic","author":"Blackburn","year":"2014"},{"key":"2025011715020773900_ref6","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF01049415","article-title":"Hybrid languages","volume":"4","author":"Blackburn","year":"1995","journal-title":"Journal of Logic, Language and Information"},{"key":"2025011715020773900_ref7","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-007-0002-4","volume-title":"Hybrid Logic and Its Proof-Theory","author":"Bra\u00fcner","year":"2011"},{"key":"2025011715020773900_ref8","volume-title":"The Computer Modelling of Mathematical Reasoning","author":"Bundy","year":"1985"},{"key":"2025011715020773900_ref9","first-page":"893","article-title":"Hybrid logic","volume-title":"Handbook of Modal Logic","author":"ten Cate","year":"2007"},{"key":"2025011715020773900_ref10","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/BF01880326","article-title":"TABLEAUX: a general theorem prover for modal logics","volume":"7","author":"Catach","year":"1991","journal-title":"Journal of Automated Reasoning"},{"key":"2025011715020773900_ref11","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00173-5","article-title":"Efficient resource management for linear logic proof search","volume":"232","author":"Cervesato","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"2025011715020773900_ref12","doi-asserted-by":"crossref","DOI":"10.1109\/LICS.2008.39","article-title":"From axioms to analytic rules in nonclassical logics","volume-title":"Logic in Computer Science\u2014LICS","author":"Ciabattoni","year":"2008"},{"key":"2025011715020773900_ref13","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1016\/j.apal.2011.09.003","article-title":"Algebraic proof theory for substructural logics: cut-elimination and completions","volume":"163","author":"Ciabattoni","year":"2012","journal-title":"Annals of Pure and Applied Logic"},{"key":"2025011715020773900_ref14","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-642-04027-6_14","article-title":"Expanding the realm of systematic proof theory","volume-title":"Computer Science Logic\u2014CSL","author":"Ciabattoni","year":"2009"},{"key":"2025011715020773900_ref15","volume-title":"Bunched Logics: A Uniform Approach","author":"Docherty","year":"2019"},{"key":"2025011715020773900_ref16","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/978-3-319-89366-2_24","article-title":"Modular tableaux calculi for separation theories","volume-title":"Foundations of Software Science and Computation Structures\u2014FoSSaCS","author":"Docherty","year":"2018"},{"key":"2025011715020773900_ref17","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/978-3-030-29026-9_19","article-title":"A non-wellfounded, labelled proof system for propositional dynamic logic","volume-title":"Automated Reasoning With Analytic Tableaux and Related Methods\u2014TABLEAUX","author":"Docherty","year":"2019"},{"key":"2025011715020773900_ref18","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198505242.001.0001","volume-title":"Elements of Intuitionism","author":"Dummett","year":"2000"},{"key":"2025011715020773900_ref19","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"Fitting","year":"1983"},{"key":"2025011715020773900_ref20","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5292-1","volume-title":"First-Order Modal Logic","author":"Fitting","year":"1998"},{"key":"2025011715020773900_ref21","volume-title":"Classical vs Non-Classical Logics: The Universality of Classical Logic (MPI-I-93-230)","author":"Gabbay"},{"key":"2025011715020773900_ref22","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems","author":"Gabbay","year":"1996"},{"key":"2025011715020773900_ref23","doi-asserted-by":"crossref","first-page":"707","DOI":"10.1093\/logcom\/13.5.707","article-title":"Semantic labelled tableaux for propositional BI$^{\\perp } $","volume":"13","author":"Galmiche","year":"2003","journal-title":"Journal of Logic and Computation"},{"key":"2025011715020773900_ref24","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1093\/logcom\/exn066","article-title":"Tableaux and resource graphs for separation logic","volume":"20","author":"Galmiche","year":"2010","journal-title":"Journal of Logic and Computation"},{"key":"2025011715020773900_ref25","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/3-540-45793-3_13","article-title":"Resource Tableaux","volume-title":"Computer Science Logic\u2014CSL","author":"Galmiche","year":"2002"},{"key":"2025011715020773900_ref26","doi-asserted-by":"crossref","first-page":"1033","DOI":"10.1017\/S0960129505004858","article-title":"The semantics of BI and resource tableaux","volume":"15","author":"Galmiche","year":"2005","journal-title":"Mathematical Structures in Computer Science"},{"key":"2025011715020773900_ref27","article-title":"Investigations into logical deduction","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"2025011715020773900_ref28","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/978-3-030-71995-1_13","article-title":"Focused proof-search in the logic of bunched implications","volume-title":"Foundations of Software Science and Computation Structures\u2014FoSSaCS","author":"Gheorghiu","year":"2021"},{"key":"2025011715020773900_ref29","article-title":"Reductive logic, coalgebra, and proof-search: a perspective from resource semantics","volume-title":"Samson Abramsky on Logic and Structure in Computer Science and Beyond","author":"Gheorghiu","year":"2021"},{"key":"2025011715020773900_ref30","first-page":"525","article-title":"Semantical analysis of the logic of bunched implications","volume-title":"Studia Logica","author":"Gheorghiu","year":"2023"},{"key":"2025011715020773900_ref31","article-title":"On the completeness of the calculus of logic","volume-title":"Kurt G\u00f6del: Collected Works: Publications 1929\u20131936","author":"G\u00f6del","year":"1986"},{"key":"2025011715020773900_ref32","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-63104-6_21","article-title":"Resource-distribution via Boolean constraints","volume-title":"Automated Deduction\u2014CADE","author":"Harland","year":"1997"},{"key":"2025011715020773900_ref33","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/601775.601778","article-title":"Resource-distribution via Boolean constraints","volume":"4","author":"Harland","year":"2003","journal-title":"ACM Transactions on Computational Logic"},{"key":"2025011715020773900_ref34","first-page":"327","volume-title":"Logic programming in intutionistic linear logic","author":"Hodas","year":"1994"},{"key":"2025011715020773900_ref35","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1006\/inco.1994.1036","article-title":"Logic programming in a fragment of intuitionistic linear logic","volume":"110","author":"Hodas","year":"1994","journal-title":"Information and Computation"},{"key":"2025011715020773900_ref36","doi-asserted-by":"crossref","DOI":"10.1007\/978-90-481-8785-0","volume-title":"Natural Deduction, Hybrid Systems and Modal Logics","author":"Indrzejczak","year":"2010"},{"key":"2025011715020773900_ref37","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-57145-0","volume-title":"Sequents and Trees","author":"Indrzejczak","year":"2021"},{"key":"2025011715020773900_ref38","volume-title":"Provability in Logic","author":"Kanger","year":"1957"},{"key":"2025011715020773900_ref39","volume-title":"Mathematical Logic","author":"Kleene","year":"2002"},{"key":"2025011715020773900_ref40","volume-title":"Logic for Problem-Solving","author":"Kowalski","year":"1986"},{"key":"2025011715020773900_ref41","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","article-title":"Linear resolution with selection function","volume":"2","author":"Kowalski","year":"1971","journal-title":"Artificial Intelligence"},{"key":"2025011715020773900_ref42","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","article-title":"Semantical analysis of modal logic I: normal modal propositional calculi","volume":"9","author":"Kripke","year":"1963","journal-title":"FoSSaCS\u2014Logic Quarterly"},{"key":"2025011715020773900_ref43","first-page":"92","article-title":"Semantical analysis of intuitionistic logic I","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Kripke","year":"1965"},{"key":"2025011715020773900_ref44","doi-asserted-by":"crossref","first-page":"1403","DOI":"10.2178\/jsl\/1067620195","article-title":"A proof-theoretic study of the correspondence of classical logic and modal logic","volume":"68","author":"Kushida","year":"2003","journal-title":"The Journal of Symbolic Logic"},{"key":"2025011715020773900_ref45","doi-asserted-by":"crossref","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","article-title":"Focusing and polarization in linear, intuitionistic, and classical logic","volume":"410","author":"Liang","year":"2009","journal-title":"Theoretical Computer Science"},{"key":"2025011715020773900_ref46","first-page":"528","article-title":"Implementing efficient resource management for linear logic programming","volume-title":"International Conference on Logic for Programming, Artificial Intelligence, and Reasoning\u2014LPAR","author":"L\u00f3pez","year":"2005"},{"key":"2025011715020773900_ref47","doi-asserted-by":"crossref","first-page":"103091","DOI":"10.1016\/j.apal.2022.103091","article-title":"From axioms to synthetic inference rules via focusing","volume":"173","author":"Marin","year":"2022","journal-title":"Annals of Pure and Applied Logic"},{"key":"2025011715020773900_ref48","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/10722086_26","article-title":"The mosaic method for temporal logics","volume-title":"Automated Reasoning With Analytic Tableaux and Related Methods\u2014TABLEAUX","author":"Marx","year":"2000"},{"key":"2025011715020773900_ref49","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1007\/3-540-58156-1_52","article-title":"Strongly analytic tableaux for normal modal logics","volume":"814","author":"Massacci","year":"1994","journal-title":"Conference on Automated Deduction\u2014CADE"},{"key":"2025011715020773900_ref50","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0743-1066(89)90031-9","article-title":"A logical analysis of modules in logic programming","volume":"6","author":"Miller","year":"1989","journal-title":"The Journal of Logic Programming"},{"key":"2025011715020773900_ref51","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","article-title":"Uniform proofs as a foundation for logic programming","volume":"51","author":"Miller","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"2025011715020773900_ref52","first-page":"411","article-title":"The use of machines to assist in rigorous proof","volume":"312","author":"Milner","year":"1984","journal-title":"Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences"},{"key":"2025011715020773900_ref53","first-page":"166","article-title":"Cut-free calculi of the S5-type","volume":"8","author":"Mints","year":"1968","journal-title":"Zapiski Nauchnykh Seminarov\u2014LOMI"},{"key":"2025011715020773900_ref54","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1023\/A:1017948105274","article-title":"Indexed systems of sequents and cut-elimination","volume":"26","author":"Mints","year":"1997","journal-title":"Journal of Philosophical Logic"},{"key":"2025011715020773900_ref55","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/s001530100124","article-title":"Contraction-free sequent calculi for geometric theories with an application to Barr\u2019s theorem","volume":"42","author":"Negri","year":"2003","journal-title":"Archive for Mathematical Logic"},{"key":"2025011715020773900_ref56","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","article-title":"Proof analysis in modal logic","volume":"34","author":"Negri","year":"2005","journal-title":"Journal of Philosophical Logic"},{"key":"2025011715020773900_ref57","doi-asserted-by":"crossref","first-page":"418","DOI":"10.2307\/420956","article-title":"Cut elimination in the presence of axioms","volume":"4","author":"Negri","year":"1998","journal-title":"Bulletin of Symbolic Logic"},{"key":"2025011715020773900_ref58","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"Negri","year":"2001"},{"key":"2025011715020773900_ref59","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","article-title":"The logic of bunched implications","volume":"5","author":"O\u2019Hearn","year":"1999","journal-title":"Bulletin of Symbolic Logic"},{"key":"2025011715020773900_ref60","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/S0022-4049(00)00161-4","article-title":"On the semantics of classical disjunction","volume":"159","author":"Pym","year":"2001","journal-title":"Journal of Pure and Applied Algebra"},{"key":"2025011715020773900_ref61","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198526339.001.0001","volume-title":"Reductive Logic and Proof-Search: Proof Theory, Semantics, and Control","author":"Pym","year":"2004"},{"key":"2025011715020773900_ref62","first-page":"107","article-title":"A games semantics for reductive logic and proof-search","volume-title":"Proceedings of the 1st Workshop on Games for Logic and Programming Languages\u2014GALOP@ETAPS","author":"Pym","year":"2005"},{"key":"2025011715020773900_ref63","volume-title":"Relevant Logic","author":"Read","year":"1988"},{"key":"2025011715020773900_ref64","volume-title":"Modal Logics as Labelled Deductive Systems","author":"Russo","year":"1996"},{"key":"2025011715020773900_ref65","article-title":"Proof-theoretic semantics","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Schroeder-Heister","year":"2018"},{"key":"2025011715020773900_ref66","article-title":"Proof-theoretic semantics","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Schroeder-Heister","year":"2018"},{"key":"2025011715020773900_ref67","volume-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","author":"Simpson","year":"1994"},{"key":"2025011715020773900_ref68","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"Troelstra","year":"2000"},{"key":"2025011715020773900_ref69","volume-title":"Logic and Structure","author":"van Dalen","year":"2012"},{"key":"2025011715020773900_ref70","volume-title":"Labelled Non-Classical Logics","author":"Vigan\u00f2","year":"2013"},{"key":"2025011715020773900_ref71","first-page":"66","article-title":"Implementing the linear logic programming language Lygon","volume-title":"Proceedings of the International Logic Programming Symposium\u2014ILPS","author":"Winikoff","year":"1995"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/1\/95\/53800146\/exad065.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/1\/95\/53800146\/exad065.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T15:02:34Z","timestamp":1737126154000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/35\/1\/95\/7446395"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,24]]},"references-count":71,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,1,17]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exad065","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2025,1]]},"published":{"date-parts":[[2023,11,24]]}}}