{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:37:32Z","timestamp":1725493052377},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","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":[[2001]]},"DOI":"10.1007\/3-540-45744-5_58","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T21:02:07Z","timestamp":1193432527000},"page":"696-700","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["STRIP: Structural Sharing for Efficient Proof-Search"],"prefix":"10.1007","author":[{"given":"D.","family":"Larchey-Wendling","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"M\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Didier","family":"Galmiche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"issue":"4","key":"58_CR1","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1093\/jigpal\/7.4.447","volume":"7","author":"A. Avellone","year":"1999","unstructured":"A. Avellone, M. Ferrari, and P. Miglioli. Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics. Logic Journal of the IGPL, 7(4):447\u2013480, 1999.","journal-title":"Logic Journal of the IGPL"},{"key":"58_CR2","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:795\u2013807, 1992.","journal-title":"Journal of Symbolic Logic"},{"key":"58_CR3","unstructured":"D. Galmiche and D. Larchey-Wendling. Formulae-as-resources management for an intuitionistic theorem prover. In 5th Workshop on Logic, Language, Information and Computation, WoLLIC\u201998, Sao Paulo, Brazil, July 1998."},{"key":"58_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","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, LNCS 1742, pages 101\u2013112, Phuket, Thailand, December 1999."},{"issue":"1","key":"58_CR5","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(n log n)-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":"58_CR6","doi-asserted-by":"crossref","unstructured":"L. Pinto and R. Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In Behara and al., editors, Symposia Gaussiana, pages 225\u2013232, 1995.","DOI":"10.1515\/9783110886726.225"},{"issue":"5","key":"58_CR7","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","volume":"2","author":"D. Sahlin","year":"1993","unstructured":"D. Sahlin, T. Franz\u00e9n, and S. Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2(5):619\u2013656, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"58_CR8","unstructured":"A. Stoughton. Porgi: a proof-or-refutation generator for intuitionistic propositional logic. In CADE Workshop on Proof-search in Type-theoretic Languages, pages 109\u2013116, Rutgers University, New Brunswick, USA, 1996."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_58","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,26]],"date-time":"2021-08-26T08:44:47Z","timestamp":1629967487000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"8 June 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}