{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:19:49Z","timestamp":1759637989871},"reference-count":42,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2012,3,1]],"date-time":"2012-03-01T00:00:00Z","timestamp":1330560000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"content-version":"vor","delay-in-days":1461,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2012,3]]},"DOI":"10.1016\/j.apal.2011.09.003","type":"journal-article","created":{"date-parts":[[2011,10,27]],"date-time":"2011-10-27T19:31:14Z","timestamp":1319743874000},"page":"266-290","source":"Crossref","is-referenced-by-count":54,"title":["Algebraic proof theory for substructural logics: Cut-elimination and completions"],"prefix":"10.1016","volume":"163","author":[{"given":"Agata","family":"Ciabattoni","sequence":"first","affiliation":[]},{"given":"Nikolaos","family":"Galatos","sequence":"additional","affiliation":[]},{"given":"Kazushige","family":"Terui","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/j.apal.2011.09.003_br000005","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/j.apal.2011.09.003_br000010","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF01531058","article-title":"Hypersequents, logical consequence and intermediate logics for concurrency","volume":"4","author":"Avron","year":"1991","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/j.apal.2011.09.003_br000015","series-title":"Proceedings of Tableaux 2011","first-page":"43","article-title":"Kripke semantics for basic sequent systems","volume":"vol. 6793","author":"Avron","year":"2011"},{"key":"10.1016\/j.apal.2011.09.003_br000020","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/978-94-007-0479-4_4","article-title":"Non-deterministic Semantics for Logical Systems","author":"Avron","year":"2011","journal-title":"Handbook of Philosophical Logic"},{"key":"10.1016\/j.apal.2011.09.003_br000025","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1002\/malq.19560020803","article-title":"H\u00fcllensysteme und Erweiterungen von Quasi-Ordnungen","volume":"2","author":"Banaschewski","year":"1956","journal-title":"Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik"},{"issue":"2","key":"10.1016\/j.apal.2011.09.003_br000030","doi-asserted-by":"crossref","first-page":"09","DOI":"10.1023\/B:STUD.0000037127.15182.2a","article-title":"Algebraic aspects of cut-elimination","volume":"77","author":"Belardinelli","year":"2004","journal-title":"Studia Logica"},{"issue":"19\u201320","key":"10.1016\/j.apal.2011.09.003_br000035","doi-asserted-by":"crossref","first-page":"2315","DOI":"10.1080\/00927878408823111","article-title":"Specially ordered groups","volume":"12","author":"Bergman","year":"1984","journal-title":"Communications in Algebra"},{"issue":"4","key":"10.1016\/j.apal.2011.09.003_br000040","first-page":"937","article-title":"MacNeille completions of Heyting algebras","volume":"30","author":"Bezhanishvili","year":"2004","journal-title":"The Houston Journal of Math."},{"key":"10.1016\/j.apal.2011.09.003_br000045","series-title":"An Introduction to Proof Theory","first-page":"1","author":"Buss","year":"1998"},{"key":"10.1016\/j.apal.2011.09.003_br000050","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3792\/pia\/1195573210","article-title":"On the completion by cuts of distributive lattices","volume":"20","author":"Funayama","year":"1944","journal-title":"Proceedings of the Imperial Academy, Tokyo"},{"key":"10.1016\/j.apal.2011.09.003_br000055","doi-asserted-by":"crossref","unstructured":"A. Ciabattoni, N. Galatos, K. Terui, MacNeille Completions of FL-algebras, Algebra Universalis (in press).","DOI":"10.1007\/s00012-011-0160-1"},{"key":"10.1016\/j.apal.2011.09.003_br000060","first-page":"229","article-title":"From axioms to analytic rules in nonclassical logics","author":"Ciabattoni","year":"2008","journal-title":"Proceedings of LICS 2008"},{"key":"10.1016\/j.apal.2011.09.003_br000065","series-title":"Proceedings of CSL 2009","first-page":"163","article-title":"Expanding the realm of systematic proof theory","volume":"vol. 5771","author":"Ciabattoni","year":"2009"},{"issue":"1","key":"10.1016\/j.apal.2011.09.003_br000070","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s11225-006-6607-2","article-title":"Towards a semantic characterization of cut-elimination","volume":"82","author":"Ciabattoni","year":"2006","journal-title":"Studia Logica"},{"issue":"1:5","key":"10.1016\/j.apal.2011.09.003_br000075","article-title":"Algorithmic correspondence and completeness in modal logic I: the core algorithm SQEMA","volume":"2","author":"Conradie","year":"2006","journal-title":"Logical Methods in Computer Science"},{"issue":"3","key":"10.1016\/j.apal.2011.09.003_br000080","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1016\/j.apal.2011.10.004","article-title":"Algorithmic correspondence and canonicity for distributive modal logic","volume":"163","author":"Conradie","year":"2012","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/j.apal.2011.09.003_br000085","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1090\/S0002-9947-05-03816-X","article-title":"MacNeille completions and canonical extensions","volume":"358","author":"Gehrke","year":"2006","journal-title":"Transactions of the American Mathematical Society"},{"issue":"2","key":"10.1016\/j.apal.2011.09.003_br000090","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/s00012-004-1870-4","article-title":"Minimal varieties of residuated lattices","volume":"52","author":"Galatos","year":"2005","journal-title":"Algebra Universalis"},{"key":"10.1016\/j.apal.2011.09.003_br000095","doi-asserted-by":"crossref","unstructured":"N. Galatos, P. Jipsen, Residuated frames with applications to decidability, Transactions of the AMS (in press).","DOI":"10.1090\/S0002-9947-2012-05573-5"},{"key":"10.1016\/j.apal.2011.09.003_br000100","series-title":"Studies in Logics and the Foundations of Mathematics","article-title":"Residuated Lattices: an algebraic glimpse at substructural logics","author":"Galatos","year":"2007"},{"key":"10.1016\/j.apal.2011.09.003_br000105","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s11225-006-8305-5","article-title":"Algebraization, parameterized local deduction theorem and interpolation for substructural logics over FL","volume":"83","author":"Galatos","year":"2006","journal-title":"Studia Logica"},{"issue":"9","key":"10.1016\/j.apal.2011.09.003_br000110","doi-asserted-by":"crossref","first-page":"1097","DOI":"10.1016\/j.apal.2010.01.003","article-title":"Cut-elimination and strong separation for substructural logics: an algebraic approach","volume":"161","author":"Galatos","year":"2010","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"10.1016\/j.apal.2011.09.003_br000115","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1023\/B:STUD.0000037126.29193.09","article-title":"Adding involution to residuated structures","volume":"77","author":"Galatos","year":"2004","journal-title":"Studia Logica"},{"key":"10.1016\/j.apal.2011.09.003_br000120","series-title":"Proceedings of the International Workshop on Interval\/Probabilistic Uncertainty and Non-classical Logics","first-page":"231","article-title":"Completions of ordered algebraic structures: a survey","volume":"vol. 46","author":"Harding","year":"2008"},{"issue":"2","key":"10.1016\/j.apal.2011.09.003_br000125","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1305\/ndjfl\/1094061862","article-title":"Extending intuitionistic linear logic with knotted structural rules","volume":"35","author":"Hori","year":"1994","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/j.apal.2011.09.003_br000130","series-title":"Ordered Algebraic Structures","first-page":"19","article-title":"A survey of residuated lattices","author":"Jipsen","year":"2002"},{"key":"10.1016\/j.apal.2011.09.003_br000135","doi-asserted-by":"crossref","first-page":"891","DOI":"10.2307\/2372123","article-title":"Boolean algebras with operators I","volume":"73","author":"J\u00f3nsson","year":"1951","journal-title":"American Journal of Math."},{"key":"10.1016\/j.apal.2011.09.003_br000140","doi-asserted-by":"crossref","first-page":"127","DOI":"10.2307\/2372074","article-title":"Boolean algebras with operators II","volume":"74","author":"J\u00f3nsson","year":"1952","journal-title":"American Journal of Math."},{"key":"10.1016\/j.apal.2011.09.003_br000145","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1090\/S0002-9947-1937-1501929-X","article-title":"Partially ordered sets","volume":"42","author":"MacNeille","year":"1937","journal-title":"Transactions of the American Mathematical Society"},{"issue":"2","key":"10.1016\/j.apal.2011.09.003_br000150","doi-asserted-by":"crossref","first-page":"790","DOI":"10.2307\/2586501","article-title":"The finite model property for various fragments of intuitionistic linear logic","volume":"64","author":"Okada","year":"1999","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/j.apal.2011.09.003_br000155","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/S0304-3975(99)00058-4","article-title":"Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic","volume":"227","author":"Okada","year":"1999","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.apal.2011.09.003_br000160","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1016\/S0304-3975(02)00024-5","article-title":"A uniform semantic proof for cut-elimination and completeness of various first and higher order logics","volume":"281","author":"Okada","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.apal.2011.09.003_br000165","series-title":"Substructural Logics","first-page":"259","article-title":"Semantics for substructural logics","author":"Ono","year":"1994"},{"key":"10.1016\/j.apal.2011.09.003_br000170","series-title":"Theories of Types and Proofs (MSJ Memoir 2)","first-page":"207","article-title":"Proof theoretic methods for nonclassical logic \u2014 an introduction","author":"Ono","year":"1998"},{"issue":"3","key":"10.1016\/j.apal.2011.09.003_br000175","doi-asserted-by":"crossref","first-page":"903","DOI":"10.2178\/jsl\/1154698583","article-title":"Correspondences between Gentzen and Hilbert systems","volume":"71","author":"Raftery","year":"2006","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/j.apal.2011.09.003_br000180","series-title":"An Introduction to Substructural Logics","author":"Restall","year":"1999"},{"key":"10.1016\/j.apal.2011.09.003_br000185","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/BF01900297","article-title":"Zur Kennzeichnung der Dedekind-MacNeilleschen H\u00fclle einer geordneten Menge","volume":"7","author":"Schmidt","year":"1956","journal-title":"Archiv der Mathematik"},{"key":"10.1016\/j.apal.2011.09.003_br000190","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/BF01969991","article-title":"Ein System des Verkn\u00fcpfenden Schliessens","volume":"2","author":"Sch\u00fctte","year":"1956","journal-title":"Archiv fur Mathematische Logik und Grundlagenforschung"},{"issue":"1","key":"10.1016\/j.apal.2011.09.003_br000195","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S1755020310000201","article-title":"Canonicity results of substructural and lattice-based logics","volume":"4","author":"Suzuki","year":"2011","journal-title":"Review of Symbolic Logic"},{"issue":"3","key":"10.1016\/j.apal.2011.09.003_br000200","doi-asserted-by":"crossref","first-page":"738","DOI":"10.2178\/jsl\/1191333839","article-title":"Which structural rules admit cut elimination? \u2014 an algebraic criterion","volume":"72","author":"Terui","year":"2007","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/j.apal.2011.09.003_br000205","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/s00012-007-2033-1","article-title":"Macneille completions of lattice expansions","volume":"57","author":"Theunissen","year":"2007","journal-title":"Algebra Universalis"},{"key":"10.1016\/j.apal.2011.09.003_br000210","series-title":"Basic Proof Theory","author":"Troelstra","year":"2000"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007211001254?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007211001254?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,11,29]],"date-time":"2018-11-29T04:26:29Z","timestamp":1543465589000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007211001254"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,3]]}},"alternative-id":["S0168007211001254"],"URL":"https:\/\/doi.org\/10.1016\/j.apal.2011.09.003","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2012,3]]}}}