{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T23:10:20Z","timestamp":1784848220484,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662488980","type":"print"},{"value":"9783662488997","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_43","type":"book-chapter","created":{"date-parts":[[2015,11,20]],"date-time":"2015-11-20T22:59:28Z","timestamp":1448060368000},"page":"622-637","source":"Crossref","is-referenced-by-count":12,"title":["SAT Modulo Intuitionistic Implications"],"prefix":"10.1007","author":[{"given":"Koen","family":"Claessen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dan","family":"Ros\u00e9n","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"issue":"3","key":"43_CR1","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0022-4049(74)90037-1","volume":"5","author":"M Barr","year":"1974","unstructured":"Barr, M.: Toposes without points. J. Pure Appl. Algebra 5(3), 265\u2013280 (1974)","journal-title":"J. Pure Appl. Algebra"},{"key":"43_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"43_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-642-16242-8_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Ferrari","year":"2010","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: fCube: an efficient prover for intuitionistic propositional logic. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 294\u2013301. Springer, Heidelberg (2010)"},{"key":"43_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-319-08587-6_19","volume-title":"Automated Reasoning","author":"R Gor\u00e9","year":"2014","unstructured":"Gor\u00e9, R., Thomson, J., Wu, J.: A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 262\u2013268. Springer, Heidelberg (2014)"},{"key":"43_CR5","doi-asserted-by":"crossref","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic - release v1.1. J. Autom. Reasoning (2006)","DOI":"10.1007\/s10817-006-9060-z"},{"key":"43_CR6","series-title":"Symbolic Computation","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466\u2013483. Springer, Heidelberg (1983)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:25:38Z","timestamp":1559316338000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}