{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T20:55:55Z","timestamp":1772916955425,"version":"3.50.1"},"reference-count":42,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[1992,4,1]],"date-time":"1992-04-01T00:00:00Z","timestamp":702086400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7777,"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":[[1992,4]]},"DOI":"10.1016\/0168-0072(92)90075-b","type":"journal-article","created":{"date-parts":[[2002,10,11]],"date-time":"2002-10-11T12:46:26Z","timestamp":1034340386000},"page":"239-311","source":"Crossref","is-referenced-by-count":143,"title":["Decision problems for propositional linear logic"],"prefix":"10.1016","volume":"56","author":[{"given":"Patrick","family":"Lincoln","sequence":"first","affiliation":[]},{"given":"John","family":"Mitchell","sequence":"additional","affiliation":[]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0168-0072(92)90075-B_BIB1","author":"Abramsky","year":"1990","journal-title":"Quantales, observational logic, and process semantics"},{"key":"10.1016\/0168-0072(92)90075-B_BIB2","article-title":"Linear objects: Logical processes with built-in inheritance","author":"Andreoli","year":"1990","journal-title":"Proc. 7th Internat. Conf. on Logic Programming"},{"key":"10.1016\/0168-0072(92)90075-B_BIB3","series-title":"Technical Report","article-title":"A logic for concurrency","author":"Asperti","year":"1987"},{"key":"10.1016\/0168-0072(92)90075-B_BIB4","first-page":"59","article-title":"Implicative formulae in the \u2018proofs as computations\u2019 analogy","author":"Asperti","year":"1990","journal-title":"Proc. 17th ACM Symp. on Principles of Programming Languages"},{"issue":"2,3","key":"10.1016\/0168-0072(92)90075-B_BIB5","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(88)90037-0","article-title":"The semantics and proof theory of linear logic","volume":"57","author":"Avron","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0168-0072(92)90075-B_BIB6","first-page":"258","article-title":"Connection graphs","author":"Bawden","year":"1986","journal-title":"Proc. ACM. Symp. on Lisp and Functional Programming"},{"key":"10.1016\/0168-0072(92)90075-B_BIB7","series-title":"Ph.D. Thesis","article-title":"Mechanizing proof theory: resource-aware logics and proof-transformations to extract implicit information","author":"Bellin","year":"1990"},{"key":"10.1016\/0168-0072(92)90075-B_BIB8","doi-asserted-by":"crossref","DOI":"10.1109\/LICS.1990.113748","article-title":"A linear semantics for allowed logic programs","author":"Cerrito","year":"1990","journal-title":"Proc. 5th IEEE Symp. on Logic in Computer Science"},{"issue":"1","key":"10.1016\/0168-0072(92)90075-B_BIB9","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","article-title":"Alternation","volume":"28","author":"Chandra","year":"1981","journal-title":"J. Assoc. Comput. Mach."},{"issue":"1","key":"10.1016\/0168-0072(92)90075-B_BIB10","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0304-3975(86)90169-6","article-title":"On the finite containment problem for Petri nets","volume":"43","author":"Clote","year":"1986","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0168-0072(92)90075-B_BIB11","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/BF01622878","article-title":"The structure of multiplicatives","volume":"28","author":"Danos","year":"1989","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/0168-0072(92)90075-B_BIB12","series-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"Garey","year":"1979"},{"key":"10.1016\/0168-0072(92)90075-B_BIB13","doi-asserted-by":"crossref","DOI":"10.1109\/LICS.1990.113746","article-title":"Normal process representatives","author":"Gehlot","year":"1990","journal-title":"Proc. 5th IEEE Symp. on Logic in Computer Science"},{"key":"10.1016\/0168-0072(92)90075-B_BIB14","series-title":"Collected Works","author":"Gentzen","year":"1969"},{"key":"10.1016\/0168-0072(92)90075-B_BIB15","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":"Theoret. Comput. Sci."},{"key":"10.1016\/0168-0072(92)90075-B_BIB16","series-title":"Multiplicatives","first-page":"11","author":"Girard","year":"1987"},{"key":"10.1016\/0168-0072(92)90075-B_BIB17","first-page":"69","article-title":"Towards a geometry of interaction","volume":"92","author":"Girard","year":"1989","journal-title":"Comtemp. Math."},{"key":"10.1016\/0168-0072(92)90075-B_BIB18","first-page":"74","article-title":"La logique lin\u00e9aire, Pour La Science","volume":"150","author":"Girard","year":"1990","journal-title":"\u00c9dition Francaise de Scientific American"},{"key":"10.1016\/0168-0072(92)90075-B_BIB19","series-title":"Cambridge Tracts Theoret. Comput. Sci.","article-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"10.1016\/0168-0072(92)90075-B_BIB20","series-title":"Proc. Math. Sci. Institute Workshop on Feasible Mathematics","article-title":"Bounded linear logic: A modular approach to polynomial time computability","author":"Girard","year":"1988-1990"},{"key":"10.1016\/0168-0072(92)90075-B_BIB21","series-title":"Proc. 10th Internat. Conf. on Application and Theory of Petri Nets","first-page":"174","article-title":"Nets as tensor theories","author":"Gunter","year":"1989"},{"key":"10.1016\/0168-0072(92)90075-B_BIB22","doi-asserted-by":"crossref","DOI":"10.1109\/LICS.1990.113759","article-title":"Single-threaded polymorphic lambda calculus","author":"Guzman","year":"1990","journal-title":"Proc. 5th IEEE Symp. on Logic in Computer Science"},{"key":"10.1016\/0168-0072(92)90075-B_BIB23","series-title":"Introduction to Combinators and Lambda Calculus, London Math. Soc. Stud. Texts","author":"Hindley","year":"1986"},{"key":"10.1016\/0168-0072(92)90075-B_BIB24","series-title":"Introduction to Automata Theory, Languages and Computation","author":"Hopcroft","year":"1979"},{"issue":"3","key":"10.1016\/0168-0072(92)90075-B_BIB25","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(84)90047-1","article-title":"A decidable fragment of predicate calculus","volume":"32","author":"Ketonen","year":"1984","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0168-0072(92)90075-B_BIB26","first-page":"267","article-title":"Decidability of reachability in vector addition systems","author":"Kosaraju","year":"1982","journal-title":"Proc. 14th ACM Symp. on Theory of Computing"},{"issue":"1,2","key":"10.1016\/0168-0072(92)90075-B_BIB27","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0304-3975(88)90100-4","article-title":"The linear abstract machine","volume":"59","author":"Lafont","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0168-0072(92)90075-B_BIB28","first-page":"95","article-title":"Interaction nets","author":"Lafont","year":"1990","journal-title":"Proc. 17th ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0168-0072(92)90075-B_BIB29","doi-asserted-by":"crossref","first-page":"154","DOI":"10.2307\/2310058","article-title":"The mathematics of sentence structure","volume":"65","author":"Lambek","year":"1958","journal-title":"Amer. Math. Monthly"},{"key":"10.1016\/0168-0072(92)90075-B_BIB30","doi-asserted-by":"crossref","first-page":"295","DOI":"10.4153\/CMB-1961-032-6","article-title":"How to program an infinite abacus","volume":"4","author":"Lambek","year":"1961","journal-title":"Canad. Math. Bull."},{"key":"10.1016\/0168-0072(92)90075-B_BIB31","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1109\/FSCS.1990.89588","article-title":"Decision problems for propositional linear logic","author":"Lincoln","year":"1990","journal-title":"Proc. 31st IEEE Symp. on Foundations of Computer Science"},{"key":"10.1016\/0168-0072(92)90075-B_BIB32","series-title":"Technical Report 62","article-title":"The reachability problem is exponential-space hard","author":"Lipton","year":"1976"},{"key":"10.1016\/0168-0072(92)90075-B_BIB33","first-page":"313","article-title":"From Petri nets to linear logic","volume":"389","author":"Mart\u00ed-Oliet","year":"1989"},{"key":"10.1016\/0168-0072(92)90075-B_BIB34","first-page":"238","article-title":"An algorithm for the general Petri net reachability problem","author":"Mayr","year":"1981","journal-title":"Proc. 13th ACM Symp. on Theory of Computing"},{"key":"10.1016\/0168-0072(92)90075-B_BIB35","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","article-title":"The complexity of the word problems for commulative semigroups and polynomial ideals","volume":"46","author":"Mayr","year":"1982","journal-title":"Adv. in Math."},{"key":"10.1016\/0168-0072(92)90075-B_BIB36","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(84)90029-X","article-title":"Petri nets and large finite sets","volume":"32","author":"McAloon","year":"1984","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0168-0072(92)90075-B_BIB37","series-title":"Ph.D. Thesis","article-title":"Topics in modal and many-valued logic","author":"Meyer","year":"1966"},{"issue":"3","key":"10.1016\/0168-0072(92)90075-B_BIB38","doi-asserted-by":"crossref","first-page":"437","DOI":"10.2307\/1970290","article-title":"Recursive unsolvability of Post's problem of \u2018tag\u2019 and other topics in the theory of Turing machines","volume":"74","author":"Minsky","year":"1961","journal-title":"Ann. of Math."},{"key":"10.1016\/0168-0072(92)90075-B_BIB39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2267170","article-title":"Recursive unsolvability of a problem of Thue","volume":"12","author":"Post","year":"1947","journal-title":"Symbolic Logic"},{"key":"10.1016\/0168-0072(92)90075-B_BIB40","first-page":"154","article-title":"A Brief guide to linear logic","volume":"41","author":"Scedrov","year":"1990","journal-title":"Bull. EATCS"},{"key":"10.1016\/0168-0072(92)90075-B_BIB41","doi-asserted-by":"crossref","first-page":"1059","DOI":"10.2307\/2274261","article-title":"The undecidability of entailment and relevant implication","volume":"49","author":"Urquhart","year":"1984","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0168-0072(92)90075-B_BIB42","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":"J. Symbolic Logic"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016800729290075B?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016800729290075B?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,5]],"date-time":"2020-03-05T08:56:39Z","timestamp":1583398599000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/016800729290075B"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,4]]},"references-count":42,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[1992,4]]}},"alternative-id":["016800729290075B"],"URL":"https:\/\/doi.org\/10.1016\/0168-0072(92)90075-b","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[1992,4]]}}}