{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:49:42Z","timestamp":1778914182740,"version":"3.51.4"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319998398","type":"print"},{"value":"9783319998404","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99840-4_7","type":"book-chapter","created":{"date-parts":[[2018,9,7]],"date-time":"2018-09-07T07:29:08Z","timestamp":1536305348000},"page":"115-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Proving Structural Properties of Sequent Systems in Rewriting Logic"],"prefix":"10.1007","author":[{"given":"Carlos","family":"Olarte","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elaine","family":"Pimentel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Camilo","family":"Rocha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,8]]},"reference":[{"issue":"3","key":"7_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J-M Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"issue":"1\u20133","key":"7_CR2","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoret. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00153-009-0137-3","volume":"48","author":"K Br\u00fcnnler","year":"2009","unstructured":"Br\u00fcnnler, K.: Deep sequent systems for modal logic. Arch. Math. Logic 48, 551\u2013577 (2009)","journal-title":"Arch. Math. Logic"},{"issue":"1","key":"7_CR4","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1006\/inco.2001.2951","volume":"179","author":"I Cervesato","year":"2002","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. Inf. Comput. 179(1), 19\u201375 (2002)","journal-title":"Inf. Comput."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., Galatos, N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: LICS, pp. 229\u2013240. IEEE Computer Society Press (2008)","DOI":"10.1109\/LICS.2008.39"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, North-Holland, pp. 68\u2013131 (1969)","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"7_CR9","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/s11787-017-0175-2","volume":"11","author":"O Lahav","year":"2017","unstructured":"Lahav, O., Marcos, J., Zohar, Y.: Sequent systems for negative modalities. Logica Universalis 11(3), 345\u2013382 (2017)","journal-title":"Logica Universalis"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-24312-2_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"B Lellmann","year":"2015","unstructured":"Lellmann, B.: Linear nested sequents, 2-sequents and hypersequents. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 135\u2013150. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_10"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1007\/978-3-662-48899-7_39","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B Lellmann","year":"2015","unstructured":"Lellmann, B., Pimentel, E.: Proof search in nested sequent calculi. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 558\u2013574. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_39"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/0168-0072(92)90075-B","volume":"56","author":"P Lincoln","year":"1992","unstructured":"Lincoln, P., Mitchell, J., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. Ann. Pure Appl. Logic 56, 239\u2013311 (1992)","journal-title":"Ann. Pure Appl. Logic"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1017\/S0027763000018055","volume":"7","author":"S Maehara","year":"1954","unstructured":"Maehara, S.: Eine darstellung der intuitionistischen logik in der klassischen. Nagoya Math. J. 7, 45\u201364 (1954)","journal-title":"Nagoya Math. J."},{"key":"7_CR14","first-page":"1","volume-title":"Handbook of Philosophical Logic","author":"N Mart\u00ed-Oliet","year":"2002","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, pp. 1\u201387. Springer, Dordrecht (2002)"},{"issue":"1","key":"7_CR15","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.tcs.2012.12.008","volume":"474","author":"D Miller","year":"2013","unstructured":"Miller, D., Pimentel, E.: A formal framework for specifying sequent calculus proof systems. Theoret. Comput. Sci. 474, 98\u2013116 (2013)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-540-74915-8_31","volume-title":"Computer Science Logic","author":"D Miller","year":"2007","unstructured":"Miller, D., Saurin, A.: From proofs to focused proofs: a modular proof of focalization in linear logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 405\u2013419. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_31"},{"issue":"2","key":"7_CR18","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1093\/logcom\/exu029","volume":"26","author":"V Nigam","year":"2016","unstructured":"Nigam, V., Pimentel, E., Reis, G.: An extended framework for specifying and reasoning about proof systems. J. Logic Comput. 26(2), 539\u2013576 (2016)","journal-title":"J. Logic Comput."},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-08587-6_18","volume-title":"Automated Reasoning","author":"V Nigam","year":"2014","unstructured":"Nigam, V., Reis, G., Lima, L.: Quati: an automated tool for proving permutation lemmas. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 255\u2013261. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_18"},{"issue":"1\/2","key":"7_CR20","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.1999.2832","volume":"157","author":"F Pfenning","year":"2000","unstructured":"Pfenning, F.: Structural cut elimination I. Intuitionistic and classical logic. Inf. Comput. 157(1\/2), 84\u2013141 (2000)","journal-title":"Inf. Comput."},{"key":"7_CR21","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"1996","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, New York (1996)"},{"issue":"2","key":"7_CR22","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theoret. Comput. Sci. 285(2), 487\u2013517 (2002)","journal-title":"Theoret. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99840-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T18:25:44Z","timestamp":1571855144000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99840-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319998398","9783319998404"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99840-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}