{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:05:40Z","timestamp":1759147540362},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540749141"},{"type":"electronic","value":"9783540749158"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74915-8_34","type":"book-chapter","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T01:13:35Z","timestamp":1187918015000},"page":"451-465","source":"Crossref","is-referenced-by-count":22,"title":["Focusing and Polarization in Intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"Chuck","family":"Liang","sequence":"first","affiliation":[]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"34_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. of Logic and Computation\u00a02(3), 297\u2013347 (1992)","journal-title":"J. of Logic and Computation"},{"key":"34_CR2","unstructured":"Chaudhuri, K.: The Focused Inverse Method for Linear Logic. PhD thesis, Carnegie Mellon University,Technical report CMU-CS-06-162 (December 2006)"},{"key":"34_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11814771_9","volume-title":"Automated Reasoning","author":"K. Chaudhuri","year":"2006","unstructured":"Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 97\u2013111. Springer, Heidelberg (2006)"},{"key":"34_CR4","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/351240.351262","volume-title":"ICFP 2000","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP 2000. Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, New York, NY, USA, pp. 233\u2013243. ACM Press, New York (2000)"},{"key":"34_CR5","series-title":"London Mathematical Society Lecture Notes 222","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1017\/CBO9780511629150.011","volume-title":"Workshop on Linear Logic","author":"V. Danos","year":"1995","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Girard, Lafont, Regnier (eds.) Workshop on Linear Logic. London Mathematical Society Lecture Notes 222, pp. 211\u2013224. Cambridge University Press, Cambridge (1995)"},{"issue":"3","key":"34_CR6","doi-asserted-by":"publisher","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V. Danos","year":"1997","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: A new deconstructive logic: Linear logic. Journal of Symbolic Logic\u00a062(3), 755\u2013807 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/11780342_19","volume-title":"Logical Approaches to Computational Barriers","author":"R. Dyckhoff","year":"2006","unstructured":"Dyckhoff, R., Lengrand, S.: LJQ: a strongly focused calculus for intuitionistic logic. In: Beckmann, A., Berger, U., L\u00f6we, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol.\u00a03988, pp. 173\u2013185. Springer, Heidelberg (2006)"},{"key":"34_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"key":"34_CR9","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"Girard, J.-Y.: A new constructive logic: classical logic. Math. Structures in Comp. Science\u00a01, 255\u2013296 (1991)","journal-title":"Math. Structures in Comp. Science"},{"key":"34_CR10","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J.-Y. Girard","year":"1993","unstructured":"Girard, J.-Y.: On the unity of logic. Annals of Pure and Applied Logic\u00a059, 201\u2013217 (1993)","journal-title":"Annals of Pure and Applied Logic"},{"key":"34_CR11","unstructured":"Herbelin, H.: S\u00e9quents qu\u2019on calcule: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de lambda-termes et comme calcul de strat\u00e9gies gagnantes. PhD thesis, Universit\u00e9 Paris 7 (1995)"},{"key":"34_CR12","unstructured":"Howe, J.M.: Proof Search Issues in Some Non-Classical Logics. PhD thesis, University of St Andrews, Available as University of St Andrews Research Report CS\/99\/1 (December 1998)"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11590156_42","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"R. Jagadeesan","year":"2005","unstructured":"Jagadeesan, R., Nadathur, G., Saraswat, V.: Testing concurrent systems: An interpretation of intuitionistic logic. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, Springer, Heidelberg (2005)"},{"issue":"2-3","key":"34_CR14","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/j.apal.2004.11.002","volume":"134","author":"O. Laurent","year":"2005","unstructured":"Laurent, O., Quatrini, M., de Falco, L.T.: Polarized and focalized linear and classical proofs. Ann. Pure Appl. Logic\u00a0134(2-3), 217\u2013264 (2005)","journal-title":"Ann. Pure Appl. Logic"},{"key":"34_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_38","volume-title":"Automata, Languages and Programming","author":"P.B. Levy","year":"2006","unstructured":"Levy, P.B.: Jumbo lambda-calculus. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, Springer, Heidelberg (2006)"},{"key":"34_CR16","unstructured":"Liang, C., Miller, D.: On focusing and polarities in linear logic and intuitionistic logic. Unpublished report (December 2006)"},{"key":"34_CR17","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic\u00a051, 125\u2013157 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"34_CR18","unstructured":"Pfenning, F.: Automated theorem proving. Lecture notes (March 2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74915-8_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:45:54Z","timestamp":1619505954000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74915-8_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540749141","9783540749158"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74915-8_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}