{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:00:22Z","timestamp":1762459222892,"version":"3.40.4"},"reference-count":33,"publisher":"Oxford University Press (OUP)","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Logic Computation"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1093\/logcom\/exu029","type":"journal-article","created":{"date-parts":[[2014,6,7]],"date-time":"2014-06-07T03:12:54Z","timestamp":1402110774000},"page":"539-576","source":"Crossref","is-referenced-by-count":20,"title":["An extended framework for specifying and reasoning about proof systems"],"prefix":"10.1093","volume":"26","author":[{"given":"Vivek","family":"Nigam","sequence":"first","affiliation":[]},{"given":"Elaine","family":"Pimentel","sequence":"additional","affiliation":[]},{"given":"Giselle","family":"Reis","sequence":"additional","affiliation":[]}],"member":"286","published-online":{"date-parts":[[2014,6,6]]},"reference":[{"key":"2016032907475274000_26.2.539.1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"2016032907475274000_26.2.539.2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs039"},{"key":"2016032907475274000_26.2.539.3","first-page":"529","article-title":"Canonical propositional Gentzen-type systems","volume-title":"IJCAR 2001","volume":"2083","author":"Avron","year":"2001"},{"key":"2016032907475274000_26.2.539.4","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00173-5"},{"key":"2016032907475274000_26.2.539.5","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"2016032907475274000_26.2.539.6","doi-asserted-by":"crossref","unstructured":"Ciabattoni A. Galatos N. Terui K. 23th Symp. on Logic in Computer Science. IEEE Computer Society Press; 2008. From axioms to analytic rules in nonclassical logics; p. 229-240.","DOI":"10.1109\/LICS.2008.39"},{"key":"2016032907475274000_26.2.539.7","first-page":"159","article-title":"The structure of exponentials: uncovering the dynamics of linear logic proofs","volume-title":"Kurt G\u00f6del Colloquium","volume":"713","author":"Danos","year":"1993"},{"key":"2016032907475274000_26.2.539.8","first-page":"173","article-title":"LJQ: a strongly focused calculus for intuitionistic logic","volume-title":"Computability in Europe 2006","volume":"3988","author":"Dyckhoff","year":"2006"},{"key":"2016032907475274000_26.2.539.9","doi-asserted-by":"publisher","DOI":"10.2307\/2695061"},{"key":"2016032907475274000_26.2.539.10","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2627"},{"key":"2016032907475274000_26.2.539.11","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-011-9208-0"},{"key":"2016032907475274000_26.2.539.12","doi-asserted-by":"crossref","unstructured":"Gentzen G. Investigations into logical deduction. In: Szabo M. E. , editor. The Collected Papers of Gerhard Gentzen. North-Holland; 1969. p. 68-131. Translation of articles that appeared in 1934-35.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"2016032907475274000_26.2.539.13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"2016032907475274000_26.2.539.14","unstructured":"Herbelin H. S\u00e9quents qu'on calcule: de l'interpr\u00e9tation du calcul des s\u00e9quents comme calcul de lambda-termes et comme calcul de strat\u00e9gies gagnantes. Universit\u00e9 Paris; 1995. p. 7. PhD Thesis."},{"key":"2016032907475274000_26.2.539.15","doi-asserted-by":"crossref","unstructured":"Lutovac T. Harland J. A contribution to automated-oriented reasoning about permutability of sequent calculi rules. Computer Science and Information Systems 2013:10.","DOI":"10.2298\/CSIS120820043L"},{"key":"2016032907475274000_26.2.539.16","doi-asserted-by":"crossref","unstructured":"Maehara S. Eine darstellung der intuitionistischen logik in der klassischen. Nagoya Mathematical Journal 1954:45-64.","DOI":"10.1017\/S0027763000018055"},{"key":"2016032907475274000_26.2.539.17","doi-asserted-by":"publisher","DOI":"10.2307\/2275915"},{"key":"2016032907475274000_26.2.539.18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45616-3_2"},{"key":"2016032907475274000_26.2.539.19","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.12.008"},{"key":"2016032907475274000_26.2.539.20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_31"},{"key":"2016032907475274000_26.2.539.21","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-005-2267-3"},{"key":"2016032907475274000_26.2.539.22","doi-asserted-by":"crossref","unstructured":"Negri S. von Plato J. Proof Analysis: A Contribution to Hilbert's Last Problem. Cambridge University Press; 2011.","DOI":"10.1017\/CBO9781139003513"},{"key":"2016032907475274000_26.2.539.23","unstructured":"Nigam V. Exploiting non-canonicity in the Sequent Calculus. 2009. PhD Thesis, Ecole Polytechnique, September."},{"key":"2016032907475274000_26.2.539.24","doi-asserted-by":"crossref","unstructured":"Nigam V. Miller D. ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP). 2009. Algorithmic specifications in linear logic with subexponentials; p. 129-140.","DOI":"10.1145\/1599410.1599427"},{"key":"2016032907475274000_26.2.539.25","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9182-1"},{"key":"2016032907475274000_26.2.539.26","first-page":"109","article-title":"Specifying proof systems in linear logic with subexponentials","volume-title":"Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop (LSFA 2010)","volume":"269","author":"Nigam","year":"2011"},{"key":"2016032907475274000_26.2.539.27","unstructured":"Nigam V. Reis G. Lima L. Checking proof transformations with ASP. TPLP 2013. 13(4-5-Online-Supplement)."},{"key":"2016032907475274000_26.2.539.28","doi-asserted-by":"crossref","unstructured":"Pfenning F. 10th Symp. on Logic in Computer Science. San Diego, California: IEEE Computer Society Press; 1995. Structural cut elimination; p. 156-166.","DOI":"10.1109\/LICS.1995.523253"},{"key":"2016032907475274000_26.2.539.29","doi-asserted-by":"crossref","unstructured":"Pfenning F. Sch\u00fcrmann C. System description: Twelf \u2014 A meta-logical framework for deductive systems. In: Ganzinger H. , editor. 16th Conf. on Automated Deduction (CADE). Trento: Springer; 1999. p. 202-206. number 1632 in LNAI.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"2016032907475274000_26.2.539.30","doi-asserted-by":"crossref","unstructured":"Pimentel E. Miller D. LPAR 2005: 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. 2005. On the specification of sequent systems; p. 352-366. number 3835 in LNAI.","DOI":"10.1007\/11591191_25"},{"key":"2016032907475274000_26.2.539.31","unstructured":"Pimentel E. G. L\u00f3gica linear e a especifica\u00e7\u00e3o de sistemas computacionais. PhD Thesis, Universidade Federal de Minas Gerais, Belo Horizonte, M.G., Brasil, December 2001. Written in English."},{"key":"2016032907475274000_26.2.539.32","unstructured":"Stewart C. Stouppa P. Advances in Modal Logic. 2004. A systematic proof theory for several modal logics; p. 309-333."},{"key":"2016032907475274000_26.2.539.33","unstructured":"Troelstra A. S. Schwichtenberg H. Basic Proof Theory. Cambridge University Press; 1996."}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/26\/2\/539\/7949477\/exu029.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T07:47:48Z","timestamp":1746258468000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article-lookup\/doi\/10.1093\/logcom\/exu029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,6]]},"references-count":33,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2016,3,29]]},"published-print":{"date-parts":[[2016,4]]}},"alternative-id":["10.1093\/logcom\/exu029"],"URL":"https:\/\/doi.org\/10.1093\/logcom\/exu029","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published":{"date-parts":[[2014,6,6]]}}}