{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:56Z","timestamp":1761611216180},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668565"},{"type":"electronic","value":"9783540466741"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46674-6_10","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T15:50:17Z","timestamp":1196351417000},"page":"101-112","source":"Crossref","is-referenced-by-count":5,"title":["Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"Didier","family":"Galmiche","sequence":"first","affiliation":[]},{"given":"Dominique","family":"Larchey-Wendling","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,11,19]]},"reference":[{"key":"10_CR1","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":"10_CR2","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."},{"issue":"1","key":"10_CR3","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"},{"issue":"1","key":"10_CR4","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1093\/jigpal\/5.1.145","volume":"5","author":"M. Ornaghi","year":"1997","unstructured":"M. Ornaghi P. Miglioli, U. Moscato. Avoiding duplications in tableaux systems for intuitionistic and Kuroda logic. Logic Journal of the IGPL, 5(1):145\u2013167, 1997.","journal-title":"Logic Journal of the IGPL"},{"key":"10_CR5","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"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"N. Shankar. Proof search in the intuitionistic sequent calculus. In 11th Conference on Automated DEduction, LNAI 607, pages 522\u2013536, Saratoga Springs, June 1992.","DOI":"10.1007\/3-540-55602-8_189"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"T. Tammet. A resolution theorem prover for intuitionistic logic. In 13th Conference on Automated Deduction, LNAI 1104, pages 2-16, NJ, USA, 1996.","DOI":"10.1007\/3-540-61511-3_65"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"C. Urban. Implementation of proof search in the imperative programming language pizza. In Int. Conference TABLEAUX\u201998, LNAI 1397, pages 313\u2013319, Oisterwijk, The Netherlands, May 1998.","DOI":"10.1007\/3-540-69778-0_31"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Proof-search in intuitionistic logic based on constraint satisfaction. In Int. Workshop TABLEAUX\u201996, LNAI 1071, pages 312\u2013327, Italy, 1996.","DOI":"10.1007\/3-540-61208-4_20"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"K. Weich. Decisions procedures for intuitionistic logic by program extraction. In Int. Conference TABLEAUX\u201998, LNAI 1397, pages 292\u2013306, Oisterwijk, The Netherlands, May 1998.","DOI":"10.1007\/3-540-69778-0_29"}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN\u201999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46674-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,26]],"date-time":"2019-02-26T00:11:37Z","timestamp":1551139897000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46674-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668565","9783540466741"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-46674-6_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}