{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:20:41Z","timestamp":1781076041564,"version":"3.54.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319085869","type":"print"},{"value":"9783319085876","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08587-6_29","type":"book-chapter","created":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T23:38:32Z","timestamp":1404257912000},"page":"374-380","source":"Crossref","is-referenced-by-count":6,"title":["Skeptik: A Proof Compression System"],"prefix":"10.1007","author":[{"given":"Joseph","family":"Boudou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Fellner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruno","family":"Woltzenlogel Paleo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-01702-5_14","volume-title":"Hardware and Software: Verification and Testing","author":"O. Bar-Ilan","year":"2009","unstructured":"Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 114\u2013128. Springer, Heidelberg (2009)"},{"issue":"3","key":"29_CR2","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-010-0167-5","volume":"13","author":"O. Bar-Ilan","year":"2011","unstructured":"Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Reducing the size of resolution proofs in linear time. STTT\u00a013(3), 263\u2013272 (2011)","journal-title":"STTT"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation, JSAT (2008)","DOI":"10.3233\/SAT190039"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-40537-2_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Boudou","year":"2013","unstructured":"Boudou, J., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs by lowering subproofs. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol.\u00a08123, pp. 59\u201373. Springer, Heidelberg (2013)"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Bouton, T., de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: verit: an open, trustable and efficient smt-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 151\u2013156. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-14186-7_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"S. Cotton","year":"2010","unstructured":"Cotton, S.: Two techniques for minimizing resolution proofs. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 306\u2013312. Springer, Heidelberg (2010)"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Dunchev, C., Leitsch, A., Libal, T., Riener, M., Rukhaia, M., Weller, D., Woltzenlogel Paleo, B.: Prooftool: a gui for the gapt framework. In: UITP, pp. 1\u201314 (2013)","DOI":"10.4204\/EPTCS.118.1"},{"key":"29_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-14203-1_36","volume-title":"Automated Reasoning","author":"T. Dunchev","year":"2010","unstructured":"Dunchev, T., Leitsch, A., Libal, T., Weller, D., Woltzenlogel Paleo, B.: System description: The proof transformation system ceres. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 427\u2013433. Springer, Heidelberg (2010)"},{"key":"29_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-22438-6_19","volume-title":"Automated Deduction \u2013 CADE-23","author":"P. Fontaine","year":"2011","unstructured":"Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs via partial regularization. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 237\u2013251. Springer, Heidelberg (2011)"},{"issue":"3","key":"29_CR10","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1137\/0209038","volume":"9","author":"J.R. Gilbert","year":"1980","unstructured":"Gilbert, J.R., Lengauer, T., Tarjan, R.E.: The pebbling problem is complete in polynomial space. SIAM Journal on Computing\u00a09(3), 513\u2013524 (1980)","journal-title":"SIAM Journal on Computing"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Goerdt, A.: Comparing the complexity of regular and unrestricted resolution. In: Marburger, H. (ed.) GWAI. Informatik-Fachberichte, vol.\u00a0251. Springer (1990)","DOI":"10.1007\/978-3-642-76071-6_20"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: Herbrand sequent extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC\/Calculemus\/MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 462\u2013477. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-85110-3_38"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Heule, M., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD, pp. 181\u2013188 (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"Hofferek, G., Gupta, A., K\u00f6nighofer, B., Jiang, J.H.R., Bloem, R.: Synthesizing multiple boolean functions using interpolation on a single proof. In: FMCAD, pp. 77\u201384 (2013)","DOI":"10.1109\/FMCAD.2013.6679394"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-19583-9_17","volume-title":"Hardware and Software: Verification and Testing","author":"S.F. Rollini","year":"2010","unstructured":"Rollini, S.F., Bruttomesso, R., Sharygina, N.: An efficient and flexible approach to resolution proof reduction. In: Raz, O. (ed.) HVC 2010. LNCS, vol.\u00a06504, pp. 182\u2013196. Springer, Heidelberg (2010)"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers in Computational Logic 1967-1970, vol.\u00a02. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"29_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-17511-4_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B. Woltzenlogel Paleo","year":"2010","unstructured":"Woltzenlogel Paleo, B.: Atomic cut introduction by resolution: Proof structuring and compression. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 463\u2013480. Springer, Heidelberg (2010)"},{"key":"29_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-35722-0_27","volume-title":"Logical Foundations of Computer Science","author":"B. Woltzenlogel Paleo","year":"2013","unstructured":"Woltzenlogel Paleo, B.: Contextual natural deduction. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol.\u00a07734, pp. 372\u2013386. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08587-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,21]],"date-time":"2020-08-21T17:32:47Z","timestamp":1598031167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08587-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319085869","9783319085876"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08587-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}