{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:29:06Z","timestamp":1725488946632},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_6","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"78-93","source":"Crossref","is-referenced-by-count":1,"title":["Embedding Lax Logic into Intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"issue":"2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1017\/S0956796898002998","volume":"8","author":"P. N. Benton","year":"1998","unstructured":"P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2):177\u2013193, 1998.","journal-title":"Journal of Functional Programming"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"249","DOI":"10.2307\/2266613","volume":"17","author":"H. B. Curry","year":"1952","unstructured":"H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249\u2013265, 1952.","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR3","unstructured":"H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957."},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57(3):795\u2013807, 1992.","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Uwe Egly. Embedding lax logic into intuitionistic logic. Technical report, Abteilung Wissensbasierte Systeme, TU Wien, 2002.","DOI":"10.1007\/3-540-45620-1_6"},{"issue":"1","key":"6_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M. Fairtlough","year":"1997","unstructured":"M. Fairtlough and M. Mendler. Propositional lax logic. Information and Computation, 137(1):1\u201333, 1997.","journal-title":"Information and Computation"},{"key":"6_CR7","unstructured":"M. Fairtlough, M. Mendler, and M. Walton. First-order lax logic as a framework for constraint logic programming. Technical Report MIPS-9714, University of Passau, 1997."},{"key":"6_CR8","unstructured":"M. Fairtlough and M. Walton. Quantified lax logic. Technical Report CS-97-11, University of Sheffield, Department of Computer Science, 1997."},{"key":"6_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/3-540-46674-6_10","volume-title":"Asian Computing Science Conference, ASIAN\u201999","author":"D. Galmiche","year":"1999","unstructured":"D. Galmiche and D. Larchey-Wendling. Structural sharing and efficient proof-search in propositional intuitionistic logic. In Asian Computing Science Conference, ASIAN\u201999, volume 1742 of Lecture Notes in Computer Science, pages 101\u2013112. Springer Verlag, 1999."},{"key":"6_CR10","unstructured":"J. M. Howe. Proof Search Issues in Some Non-Classical Logics. PhD thesis, University of St Andrews, December 1998. Available as University of St Andrews Research Report CS\/99\/1."},{"issue":"4","key":"6_CR11","first-page":"573","volume":"11","author":"J. M. Howe","year":"2001","unstructured":"J. M. Howe. Proof search in lax logic. Mathematical Structures in Computer Science, 11(4):573\u2013588, August 2001.","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"6_CR12","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J. Hudelmaier","year":"1993","unstructured":"J. Hudelmaier. An O(nlogn)-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, 3(1):63\u201375, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"6_CR13","unstructured":"M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Edinburgh University, Department of Computer Science, ECS-LFCS-93-255, 1993."},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"E. Moggi. Notion of computation and monads. Information and Computation, 93:55\u201392, 1991.","journal-title":"Information and Computation"},{"issue":"4","key":"6_CR15","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F. Pfenning","year":"2001","unstructured":"F. Pfenning and R. Davis. A judgemental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511\u2013540, August 2001.","journal-title":"Mathematical Structures in Computer Science"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1979","unstructured":"R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9:67\u201372, 1979.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:56:16Z","timestamp":1556754976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}