{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:55Z","timestamp":1761611155670,"version":"build-2065373602"},"reference-count":22,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":5688,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1998]]},"DOI":"10.1016\/s1571-0661(05)01179-5","type":"journal-article","created":{"date-parts":[[2005,4,13]],"date-time":"2005-04-13T14:20:46Z","timestamp":1113402046000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":3,"special_numbering":"C","title":["Proof nets Construction and Automated Deduction in Non-Commutative Linear Logic"],"prefix":"10.1016","volume":"17","author":[{"given":"D.","family":"Galmiche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B.","family":"Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S1571-0661(05)01179-5_bib1","doi-asserted-by":"crossref","first-page":"1403","DOI":"10.2307\/2275485","article-title":"Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic","volume":"56","author":"Abrusci","year":"1991","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(05)01179-5_bib2","series-title":"Advances in Linear Logic","first-page":"271","article-title":"Noncommutative proof nets","author":"Abrusci","year":"1995"},{"key":"10.1016\/S1571-0661(05)01179-5_bib3","unstructured":"V.M. Abrusci. Lambek calculus, cyclic multiplicative-additive linear logic, noncommutative multiplicative-additive linear logic: language and sequent calculus. In V.M. Abrusci and C. Casadio, editors, Proofs and Linguistic Categories \u2013 Proceedings 1996 Roma Workshop, pages 21\u201348, 1996."},{"key":"10.1016\/S1571-0661(05)01179-5_bib4","doi-asserted-by":"crossref","unstructured":"A. Asperti and G. Dore. Yet another correctness criterion for multiplicative linear logic with mix. In Logic at St Petersburg '94, Symposium on Logical Foundations of Computer Science, LNCS 813, pages 34\u201346, St Petersburg, Russia, July 1994.","DOI":"10.1007\/3-540-58140-5_5"},{"key":"10.1016\/S1571-0661(05)01179-5_bib5","series-title":"Advances in Linear Logic","first-page":"249","article-title":"Subnets of proof-nets in MLL\u2212","author":"Bellin","year":"1995"},{"key":"10.1016\/S1571-0661(05)01179-5_bib6","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/BF01622878","article-title":"The structures of multiplicatives","volume":"28","author":"Danos","year":"1989","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S1571-0661(05)01179-5_bib7","unstructured":"D. Galmiche. Connection methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 1998. Accepted for publication."},{"key":"10.1016\/S1571-0661(05)01179-5_bib8","unstructured":"D. Galmiche and B. Martin. Automated proof nets construction in multiplicative and additive linear logic. Technical report, CRIN-CNRS, 1997."},{"key":"10.1016\/S1571-0661(05)01179-5_bib9","doi-asserted-by":"crossref","unstructured":"D. Galmiche and B. Martin. Proof search and proof nets construction in linear logic. In 4th Workshop on Logic, Language, Information and Computation, Wollic'97, Fortaleza, Brasil, August 1997. Logic Journal of IGPL, vol. 5\u20136, pp 883\u2013885.","DOI":"10.1093\/jigpal\/5.6.859"},{"key":"10.1016\/S1571-0661(05)01179-5_bib10","doi-asserted-by":"crossref","unstructured":"D. Galmiche and G. Perrier. A procedure for automatic proof nets construction. In LPAR'92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, pages 42\u201353, St. Petersburg, Russia, July 1992.","DOI":"10.1007\/BFb0013047"},{"issue":"1","key":"10.1016\/S1571-0661(05)01179-5_bib11","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(94)00105-7","article-title":"On proof normalization in linear logic","volume":"135","author":"Galmiche","year":"1994","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/S1571-0661(05)01179-5_bib12","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":"10.1016\/S1571-0661(05)01179-5_bib13","doi-asserted-by":"crossref","unstructured":"J.Y. Girard. Towards a geometry of interaction. In J.W. Gray and A. Scedrov, editors, Conference on Categories in Computer Science and Logic, pages 69\u2013108, Boulder, Colorado, June 1987.","DOI":"10.1090\/conm\/092\/1003197"},{"key":"10.1016\/S1571-0661(05)01179-5_bib14","series-title":"Advances in Linear Logic","first-page":"1","article-title":"Linear logic: its syntax and semantics","author":"Girard","year":"1995"},{"key":"10.1016\/S1571-0661(05)01179-5_bib15","series-title":"Logic and Algebra","article-title":"Proof nets: the parallel syntax for proof theory","author":"Girard","year":"1995"},{"key":"10.1016\/S1571-0661(05)01179-5_bib16","doi-asserted-by":"crossref","unstructured":"G. Gonthier, M. Abadi, and J.J. Levy. Linear logic without boxes. In 7th IEEE Symposium on Logic in Computer Science, pages 223\u2013234, Santa-Cruz, California, June 1992.","DOI":"10.1109\/LICS.1992.185535"},{"key":"10.1016\/S1571-0661(05)01179-5_bib17","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0168-0072(92)90075-B","article-title":"Decision problems for propositional linear logic","volume":"56","author":"Lincoln","year":"1992","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2,3","key":"10.1016\/S1571-0661(05)01179-5_bib18","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1093\/jigpal\/3.2-3.403","article-title":"Clausal proofs and discontinuity","volume":"3","author":"Morrill","year":"1995","journal-title":"L. J. of the IGPL"},{"key":"10.1016\/S1571-0661(05)01179-5_bib19","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/S1571-0661(05)82518-6","article-title":"A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic \u2013 extended abstract","volume":"3","author":"Nagayama","year":"1996","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)01179-5_bib20","doi-asserted-by":"crossref","unstructured":"M. Pentus. Equivalence of multiplicative fragments of cyclic linear logic and noncommutative linear logic. In 4th Int. Symposium LFCS'97, LNCS 1234, pages 306\u2013311, Yaroslavl, Russia, 1997.","DOI":"10.1007\/3-540-63045-7_31"},{"issue":"2","key":"10.1016\/S1571-0661(05)01179-5_bib21","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1093\/logcom\/2.2.211","article-title":"Proof Nets for Lambek Calculus","volume":"2","author":"Roorda","year":"1992","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"10.1016\/S1571-0661(05)01179-5_bib22","doi-asserted-by":"crossref","first-page":"41","DOI":"10.2307\/2274953","article-title":"Quantales and (noncommutative) linear logic","volume":"55","author":"Yetter","year":"1990","journal-title":"Journal of Symbolic Logic"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105011795?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105011795?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:06:31Z","timestamp":1761609991000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105011795"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"references-count":22,"alternative-id":["S1571066105011795"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)01179-5","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Proof nets Construction and Automated Deduction in Non-Commutative Linear Logic","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)01179-5","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1998 Elsevier Science B.V. Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}