{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:39:08Z","timestamp":1725975548820},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319906850"},{"type":"electronic","value":"9783319906867"}],"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-90686-7_2","type":"book-chapter","created":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T13:49:55Z","timestamp":1524491395000},"page":"17-32","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Direct Encodings of NP-Complete Problems into Horn Sequents of Multiplicative Linear Logic"],"prefix":"10.1007","author":[{"given":"Satoshi","family":"Matsuoka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,24]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Kanovich, M.I.: Horn programming in linear logic is NP-complete. In: Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp. 200\u2013210 (1992)","key":"2_CR1","DOI":"10.1109\/LICS.1992.185533"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/0168-0072(94)90085-X","volume":"69","author":"MI Kanovich","year":"1994","unstructured":"Kanovich, M.I.: The complexity of Horn fragments of linear logic. Ann. Pure Appl. Logic 69, 195\u2013241 (1994)","journal-title":"Ann. Pure Appl. Logic"},{"key":"2_CR3","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"MR Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, New York (1979)"},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"987","DOI":"10.1016\/S0304-3975(00)00381-9","volume":"266","author":"T Krantz","year":"2001","unstructured":"Krantz, T., Mogbil, V.: Encoding Hamiltonian circuits into multiplicative linear logic. Theoret. Comput. Sci. 266, 987\u2013996 (2001)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52, 76\u201382 (2009)","journal-title":"Commun. ACM"},{"unstructured":"Matsuoka, S.: Proof Net Calculator (2017). \nhttps:\/\/staff.aist.go.jp\/s-matsuoka\/PNCalculator\/index.html","key":"2_CR6"},{"issue":"1","key":"2_CR7","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.apal.2006.06.001","volume":"145","author":"S Matsuoka","year":"2007","unstructured":"Matsuoka, S.: Weak typed B\u00f6hm theorem on IMLL. Ann. Pure Appl. Logic 145(1), 37\u201390 (2007)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"2_CR8","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1017\/S0960129511000582","volume":"22","author":"S Matsuoka","year":"2012","unstructured":"Matsuoka, S.: A coding theoretic study of MLL proof nets. Math. Struct. Comput. Sci. 22(3), 409\u2013449 (2012)","journal-title":"Math. Struct. Comput. Sci."},{"unstructured":"Girard, J.Y.: Multiplicatives. In: Logic and Computer Science: New Trends and Applications, pp. 11\u201334 (1988)","key":"2_CR9"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.207.1","volume":"207","author":"Satoshi Matsuoka","year":"2016","unstructured":"Matsuoka, S.: Strong typed B\u00f6hm theorem and functional completeness on the linear lambda calculus. In: Proceedings of 6th Workshop on Mathematically Structured Functional Programming, MSFP 2016, pp. 1\u201322 (2016)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"2_CR11","volume-title":"Programming in Scala","author":"M Odersky","year":"2016","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala, 3rd edn. Artima Inc., Walnut Creek (2016)","edition":"3"},{"key":"2_CR12","volume-title":"Proofs and Types","author":"JY Girard","year":"1989","unstructured":"Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1989)"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1145\/1149114.1149116","volume":"7","author":"AM Murawski","year":"2006","unstructured":"Murawski, A.M., Ong, C.H.L.: Fast verification of MLL proof nets via IMLL. ACM Trans. Comput. Logic 7, 473\u2013498 (2006)","journal-title":"ACM Trans. Comput. Logic"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BF01622878","volume":"28","author":"V Danos","year":"1989","unstructured":"Danos, V., Regnier, R.: The structure of multiplicatives. Arch. Math. Logic 28, 181\u2013203 (1989)","journal-title":"Arch. Math. Logic"},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-1-4684-2001-2_9","volume-title":"Complexity of Computer Computations: Proceedings of a Symposium on the Complexity of Computer Computations","author":"RM Karp","year":"1972","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W., Bohlinger, J.D. (eds.) Complexity of Computer Computations: Proceedings of a Symposium on the Complexity of Computer Computations, pp. 85\u2013103. Springer, Boston (1972)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-90686-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T13:50:22Z","timestamp":1524491422000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-90686-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319906850","9783319906867"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-90686-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}