{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:12:28Z","timestamp":1761610348752,"version":"build-2065373602"},"reference-count":20,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"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":4958,"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":[[2000]]},"DOI":"10.1016\/s1571-0661(05)01137-0","type":"journal-article","created":{"date-parts":[[2005,4,8]],"date-time":"2005-04-08T09:19:45Z","timestamp":1112951985000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":5,"special_numbering":"C","title":["Proof-search and Proof Nets in Mixed Linear Logic"],"prefix":"10.1016","volume":"37","author":[{"given":"D.","family":"Galmiche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.M.","family":"Notin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)01137-0_bib1","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0168-0072(99)00014-7","article-title":"Non-commutative logic I: the multiplicative fragment","volume":"101","author":"Abrusci","year":"2000","journal-title":"Annals of Pure and Applied Logic"},{"issue":"4","key":"10.1016\/S1571-0661(05)01137-0_bib2","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"},{"issue":"1","key":"10.1016\/S1571-0661(05)01137-0_bib3","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1093\/jigpal\/2.1.77","article-title":"Applications of Linear Logic to Computation: An Overview","volume":"2","author":"Alexiev","year":"1994","journal-title":"Logic Journal of the IGPL"},{"year":"2000","series-title":"Labelled Deduction, volume 17 of Applied Logic Series","author":"Balat","key":"10.1016\/S1571-0661(05)01137-0_bib4"},{"key":"10.1016\/S1571-0661(05)01137-0_bib5","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/0168-0072(94)00033-Y","article-title":"Sequent reconstruction in LLM \u2013 a sweepline proof","volume":"73","author":"Banach","year":"1995","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1571-0661(05)01137-0_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)01137-0_bib7","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1017\/S0960129599002789","article-title":"A specification logic for concurrent object-oriented programming","volume":"9","author":"Delzanno","year":"1999","journal-title":"Math. Struct. in Comp. Science"},{"issue":"1\u20132","key":"10.1016\/S1571-0661(05)01137-0_bib8","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/S0304-3975(99)00176-0","article-title":"Connection Methods in Linear Logic and Proof nets Construction","volume":"232","author":"Galmiche","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)01137-0_bib9","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(05)01179-5","article-title":"Proof nets construction and automated deduction in non-commutative linear logic \u2013 extended abstract","volume":"17","author":"Galmiche","year":"1998","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)01137-0_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"},{"key":"10.1016\/S1571-0661(05)01137-0_bib11","doi-asserted-by":"crossref","unstructured":"D. Galmiche and G. Perrier. Foundations of proof search strategies design in linear logic. In Logic at St Petersburg '94, Symposium on Logical Foundations of Computer Science, LNCS 813, pages 101\u2013113, St Petersburg, Russia, July 1994.","DOI":"10.1007\/3-540-58140-5_11"},{"key":"10.1016\/S1571-0661(05)01137-0_bib12","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)01137-0_bib13","series-title":"Logic and Algebra","article-title":"Proof nets: the parallel syntax for proof theory","author":"Girard","year":"1995"},{"issue":"3","key":"10.1016\/S1571-0661(05)01137-0_bib14","first-page":"88","article-title":"Connection-based theorem proving in classical and non-classical logics","volume":"5","author":"Kreitz","year":"1999","journal-title":"Journal of Universal Computer Science"},{"issue":"1","key":"10.1016\/S1571-0661(05)01137-0_bib15","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","article-title":"Forum: A multiple-conclusion specification logic","volume":"165","author":"Miller","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)01137-0_bib16","doi-asserted-by":"crossref","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)01137-0_bib17","unstructured":"P. Ruet. Logique non-commutative et programmation par contraintes. PhD thesis, Universit\u00e9 Denis Diderot, Paris 7, 1997."},{"key":"10.1016\/S1571-0661(05)01137-0_bib18","doi-asserted-by":"crossref","unstructured":"P. Ruet and F. Fages. Concurrent constraint programming and noncommutative logic. In 11th Int. Workshop on Computer Science Logic, CSL'97, LNCS 1414, pages 406\u2013423, Aarhus, Denmark, August 1997.","DOI":"10.1007\/BFb0028028"},{"key":"10.1016\/S1571-0661(05)01137-0_bib19","series-title":"4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918","first-page":"106","article-title":"On transforming intuitionistic matrix proofs into standard sequent proofs","author":"Schmitt","year":"1995"},{"issue":"1","key":"10.1016\/S1571-0661(05)01137-0_bib20","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:S1571066105011370?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105011370?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:29Z","timestamp":1761609989000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105011370"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"references-count":20,"alternative-id":["S1571066105011370"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)01137-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Proof-search and Proof Nets in Mixed 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)01137-0","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2000 Elsevier Science B.V. Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}