{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T04:11:08Z","timestamp":1750392668360,"version":"3.41.0"},"reference-count":66,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,6,27]],"date-time":"2017-06-27T00:00:00Z","timestamp":1498521600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Austrian Science Fund"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s10009-017-0459-0","type":"journal-article","created":{"date-parts":[[2017,6,27]],"date-time":"2017-06-27T09:20:35Z","timestamp":1498555235000},"page":"71-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Greedy pebbling for proof space compression"],"prefix":"10.1007","volume":"21","author":[{"given":"Andreas","family":"Fellner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Woltzenlogel\u00a0Paleo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,27]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: The matita interactive theorem prover. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction\u2014CADE-23\u201423rd International Conference on Automated Deduction, Wroclaw, Poland, July 31\u2013August 5, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6803, pp. 64\u201369. Springer (2011)","key":"459_CR1","DOI":"10.1007\/978-3-642-22438-6_7"},{"unstructured":"Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., Saillard, R.: Dedukti: a logical framework based on the $$\\lambda \\pi $$ \u03bb \u03c0 -calculus modulo theory. http:\/\/www.lsv.fr\/~dowek\/Publi\/expressing.pdf (2016)","key":"459_CR2"},{"doi-asserted-by":"crossref","unstructured":"Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: Haifa Verification Conference, pp. 114\u2013128 (2008)","key":"459_CR3","DOI":"10.1007\/978-3-642-01702-5_14"},{"doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification\u201423rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177. Springer (2011)","key":"459_CR4","DOI":"10.1007\/978-3-642-22110-1_14"},{"unstructured":"Barrett, C., Fontaine, P., de\u00a0Moura, L.: Proofs in satisfiability modulo theories. In: Woltzenlogel\u00a0Paleo, B., Delahaye, D. (eds.) All About Proofs, Proofs for All, Mathematical Logic and Foundations, vol.\u00a055. College Publications, London, UK. http:\/\/www.collegepublications.co.uk\/logic\/mlf\/?00023 (2015)","key":"459_CR5"},{"doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E.: Size space tradeoffs for resolution. In: STOC, pp. 457\u2013464 (2002)","key":"459_CR6","DOI":"10.1145\/509907.509975"},{"key":"459_CR7","first-page":"2","volume":"16","author":"E Ben-Sasson","year":"2009","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Short proofs may be spacious: an optimal separation of space and length in resolution. Electron. Colloq. Comput. Complex. 16, 2 (2009)","journal-title":"Electron. Colloq. Comput. Complex."},{"issue":"2\u20134","key":"459_CR8","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"unstructured":"Biere, A., Heule, M.: Satisfiability solvers. In: Woltzenlogel\u00a0Paleo, B., Delahaye, D. (eds.) All About Proofs, Proofs for All, Mathematical Logic and Foundations, vol.\u00a055. College Publications, London, UK. http:\/\/www.collegepublications.co.uk\/logic\/mlf\/?00023 (2015)","key":"459_CR9"},{"volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)","key":"459_CR10"},{"unstructured":"Blanchette, J.C., Urban, J. (eds.): Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9\u201310, 2013, EPiC Series in Computing, vol.\u00a014. EasyChair. http:\/\/www.easychair.org\/publications\/?page=771427785 (2013)","key":"459_CR11"},{"doi-asserted-by":"publisher","unstructured":"Boudou, J., Fellner, A., Woltzenlogel\u00a0Paleo, B.: Skeptik: A proof compression system. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR. Lecture Notes in Computer Science, vol. 8562, pp. 374\u2013380. Springer. doi: 10.1007\/978-3-319-08587-6 (2014)","key":"459_CR12","DOI":"10.1007\/978-3-319-08587-6"},{"doi-asserted-by":"publisher","unstructured":"Boudou, J., Woltzenlogel\u00a0Paleo, B.: Compression of propositional resolution proofs by lowering subproofs. In: Galmiche and Larchey-Wendling [30], pp. 59\u201373. doi: 10.1007\/978-3-642-40537-2_7 (2013)","key":"459_CR13","DOI":"10.1007\/978-3-642-40537-2_7"},{"doi-asserted-by":"crossref","unstructured":"Bouton, T., de\u00a0Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: Verit: an open, trustable and efficient SMT-solver. In: CADE, pp. 151\u2013156 (2009)","key":"459_CR14","DOI":"10.1007\/978-3-642-02959-2_12"},{"doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, pp. 1\u20135. ACM (2009)","key":"459_CR15","DOI":"10.1145\/1670412.1670413"},{"doi-asserted-by":"crossref","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Theory and Applications of Satisfiability Testing\u2014SAT 2010, pp. 44\u201357. Springer (2010)","key":"459_CR16","DOI":"10.1007\/978-3-642-14186-7_6"},{"doi-asserted-by":"crossref","unstructured":"Burel, G.: A shallow embedding of resolution and superposition proofs into the $${\\lambda \\Pi } $$ \u03bb \u03a0 -calculus modulo. In: Blanchette, J.C., Urban, J. (eds.) Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9\u201310, 2013. EPiC Series in Computing, vol.\u00a014, pp. 43\u201357. EasyChair. http:\/\/www.easychair.org\/publications\/?page=1045498133 (2013)","key":"459_CR17","DOI":"10.29007\/ftc2"},{"unstructured":"Chan, S.M.: Pebble games and complexity. Technical Report UCB\/EECS-2013-145, University of California, Berkeley, EECS Department, University of California, Berkeley, USA (2013)","key":"459_CR18"},{"doi-asserted-by":"publisher","unstructured":"Chihani, Z., Libal, T., Reis, G.: The proof certifier checkers. In: de\u00a0Nivelle, H. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods\u201424th International Conference, TABLEAUX 2015, Wroc\u0142aw, Poland, September 21\u201324, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9323, pp. 201\u2013210. Springer. doi: 10.1007\/978-3-319-24312-2_14 (2015)","key":"459_CR19","DOI":"10.1007\/978-3-319-24312-2_14"},{"doi-asserted-by":"crossref","unstructured":"Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) Automated Deduction\u2014CADE-24\u201424th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9\u201314, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7898, pp. 162\u2013177. Springer (2013)","key":"459_CR20","DOI":"10.1007\/978-3-642-38574-2_11"},{"doi-asserted-by":"crossref","unstructured":"Cotton, S.: Two techniques for minimizing resolution proofs. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 306\u2013312. Springer (2010)","key":"459_CR21","DOI":"10.1007\/978-3-642-14186-7_26"},{"doi-asserted-by":"publisher","unstructured":"Dowek, G., Dubois, C., Pientka, B., Rabe, F. Universality of Proofs (Dagstuhl Seminar 16421). Dagstuhl Rep. 6(10), 75\u201398 (2017) doi: 10.4230\/DagRep.6.10.75","key":"459_CR22","DOI":"10.4230\/DagRep.6."},{"doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M.V. (eds.) Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17\u201319, 2010. Proceedings. Lecture Notes in Computer Science, vol. 5944, pp. 129\u2013145. Springer (2010)","key":"459_CR23","DOI":"10.1007\/978-3-642-11319-2_12"},{"doi-asserted-by":"publisher","unstructured":"Dunchev, C., Leitsch, A., Libal, T., Riener, M., Rukhaia, M., Weller, D., Paleo, B.W.: PROOFTOOL: a GUI for the GAPT framework. In: Kaliszyk, C., L\u00fcth, C. (eds.) Proceedings 10th International Workshop On User Interfaces for Theorem Provers, UITP 2012, Bremen, Germany, July 11th, 2012. EPTCS, vol. 118, pp. 1\u201314. doi: 10.4204\/EPTCS.118.1 (2012)","key":"459_CR24","DOI":"10.4204\/EPTCS.118.1"},{"doi-asserted-by":"publisher","unstructured":"Dunchev, T., Leitsch, A., Libal, T., Weller, D., Woltzenlogel\u00a0Paleo, B.: System description: the proof transformation system CERES. In: Giesl, J., H\u00e4hnle, R. (eds.) Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16\u201319, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6173, pp. 427\u2013433. Springer. doi: 10.1007\/978-3-642-14203-1_36 (2010)","key":"459_CR25","DOI":"10.1007\/978-3-642-14203-1_36"},{"doi-asserted-by":"publisher","unstructured":"Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning\u20148th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27\u2013July 2, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9706, pp. 293\u2013301. Springer. doi: 10.1007\/978-3-319-40229-1_20 (2016)","key":"459_CR26","DOI":"10.1007\/978-3-319-40229-1_20"},{"key":"459_CR27","first-page":"101","volume-title":"Theoretical Computer Science. Lecture Notes in Computer Science","author":"P Emde Boas van","year":"1979","unstructured":"van Emde Boas, P., van Leeuwen, J.: Move rules and trade-offs in the pebble game. In: Weihrauch, K. (ed.) Theoretical Computer Science. Lecture Notes in Computer Science, vol. 67, pp. 101\u2013112. Springer, Berlin (1979)"},{"issue":"1","key":"459_CR28","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.2001.2921","volume":"171","author":"JL Esteban","year":"2001","unstructured":"Esteban, J.L., Tor\u00e1n, J.: Space bounds for resolution. Inf. Comput. 171(1), 84\u201397 (2001)","journal-title":"Inf. Comput."},{"doi-asserted-by":"crossref","unstructured":"Fontaine, P., Merz, S., Woltzenlogel\u00a0Paleo, B.: Compression of propositional resolution proofs via partial regularization. In: CADE, pp. 237\u2013251 (2011)","key":"459_CR29","DOI":"10.1007\/978-3-642-22438-6_19"},{"doi-asserted-by":"publisher","unstructured":"Galmiche, D., Larchey-Wendling, D. (eds.): Automated Reasoning with Analytic Tableaux and Related Methods\u201422nd International Conference, TABLEAUX 2013, Nancy, France, September 16\u201319, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8123. Springer. doi: 10.1007\/978-3-642-40537-2 (2013)","key":"459_CR30","DOI":"10.1007\/978-3-642-40537-2"},{"issue":"3","key":"459_CR31","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1137\/0209038","volume":"9","author":"JR Gilbert","year":"1980","unstructured":"Gilbert, J.R., Lengauer, T., Tarjan, R.E.: The pebbling problem is complete in polynomial space. SIAM J. Comput. 9(3), 513\u2013524 (1980)","journal-title":"SIAM J. Comput."},{"doi-asserted-by":"publisher","unstructured":"Gorzny, J., Woltzenlogel\u00a0Paleo, B.: Towards the compression of first-order resolution proofs by lowering unit clauses. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction\u2014CADE-25\u201425th International Conference on Automated Deduction, Berlin, Germany, August 1\u20137, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9195, pp. 356\u2013366. Springer. doi: 10.1007\/978-3-319-21401-6_24 (2015)","key":"459_CR32","DOI":"10.1007\/978-3-319-21401-6_24"},{"unstructured":"Hertel, P., Pitassi, T.: Black-white pebbling is PSPACE-complete. Electron. Colloq. Comput. Complex. 14(044). http:\/\/eccc.hpiweb.de\/eccc-reports\/2007\/TR07-044\/index.html (2007)","key":"459_CR33"},{"key":"459_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2014.05.018","volume":"549","author":"S Hetzl","year":"2014","unstructured":"Hetzl, S., Leitsch, A., Reis, G., Weller, D.: Algorithmic introduction of quantified cuts. Theor. Comput. Sci. 549, 1\u201316 (2014). doi: 10.1016\/j.tcs.2014.05.018","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel\u00a0Paleo, B.: Herbrand sequent extraction. In: Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28\u2013August 1, 2008. Proceedings, pp. 462\u2013477. doi: 10.1007\/978-3-540-85110-3_38 (2008)","key":"459_CR35","DOI":"10.1007\/978-3-540-85110-3_38"},{"doi-asserted-by":"publisher","unstructured":"Hetzl, S., Libal, T., Riener, M., Rukhaia, M.: Understanding resolution proofs through Herbrand\u2019s theorem. In: Galmiche and Larchey-Wendling [30], pp. 157\u2013171. doi: 10.1007\/978-3-642-40537-2_15 (2013)","key":"459_CR36","DOI":"10.1007\/978-3-642-40537-2_15"},{"unstructured":"Heule, M.J.H.: The DRAT format and drat-trim checker. CoRR abs\/1610.06229. http:\/\/arxiv.org\/abs\/1610.06229 (2016)","key":"459_CR37"},{"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. CoRR abs\/1308.4767 (2013)","key":"459_CR38","DOI":"10.1109\/FMCAD.2013.6679394"},{"unstructured":"Huet, G., Paulin-Mohring, C., et\u00a0al.: The Coq proof assistant reference manual. Part Coq Syst. Version 6(1). https:\/\/pdfs.semanticscholar.org\/fa95\/827bfe2b83c2e27e4d17214fb22eca13cc87.pdf (2000)","key":"459_CR39"},{"doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Paskevich, A. (eds.): Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2\u20133, 2015, EPTCS, vol. 186. doi: 10.4204\/EPTCS.186 (2015)","key":"459_CR40","DOI":"10.4204\/EPTCS.186"},{"issue":"1","key":"459_CR41","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"issue":"4","key":"459_CR42","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1137\/0208046","volume":"8","author":"T Kasai","year":"1979","unstructured":"Kasai, T., Adachi, A., Iwata, S.: Classes of pebble games and complete problems. SIAM J. Comput. 8(4), 574\u2013586 (1979)","journal-title":"SIAM J. Comput."},{"key":"459_CR43","volume-title":"The Resolution Calculus. Texts in Theoretical Computer Science","author":"A Leitsch","year":"1997","unstructured":"Leitsch, A.: The Resolution Calculus. Texts in Theoretical Computer Science. Springer, Berlin (1997)"},{"doi-asserted-by":"publisher","unstructured":"Libal, T., Riener, M., Rukhaia, M.: Advanced proof viewing in proof tool. In: Benzm\u00fcller, C., Paleo, B.W. (eds.) Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, 17th July 2014. EPTCS, vol. 167, pp. 35\u201347. doi: 10.4204\/EPTCS.167.6 (2014)","key":"459_CR44","DOI":"10.4204\/EPTCS.167.6"},{"unstructured":"Miller, D.: Foundational proof certificates. In: Woltzenlogel\u00a0Paleo, B., Delahaye, D. (eds.) All About Proofs, Proofs for All, Mathematical Logic and Foundations, vol.\u00a055. College Publications, London, UK. http:\/\/www.collegepublications.co.uk\/logic\/mlf\/?00023 (2015)","key":"459_CR45"},{"doi-asserted-by":"crossref","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press. http:\/\/www.cambridge.org\/de\/academic\/subjects\/computer-science\/programming-languages-and-applied-logic\/programming-higher-order-logic?format=HB (2012)","key":"459_CR46","DOI":"10.1017\/CBO9781139021326"},{"doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Lee, P., Henglein, F., Jones, N.D. (eds.) Conference Record of POPL\u201997: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15\u201317 January 1997. pp. 106\u2013119. ACM Press (1997)","key":"459_CR47","DOI":"10.1145\/263699.263712"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer (2002)","key":"459_CR48","DOI":"10.1007\/3-540-45949-9"},{"issue":"1","key":"459_CR49","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1137\/060668250","volume":"39","author":"J Nordstr\u00f6m","year":"2009","unstructured":"Nordstr\u00f6m, J.: Narrow proofs may be spacious: separating space and width in resolution. SIAM J. Comput. 39(1), 59\u2013121 (2009)","journal-title":"SIAM J. Comput."},{"unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. IWIL-2010 (2010)","key":"459_CR50"},{"unstructured":"Philipp, T., Rebola-Pardo, A.: Towards a semantics of unsatisfiability proofs with inprocessing (2017)","key":"459_CR51"},{"doi-asserted-by":"crossref","unstructured":"Pientka, B.: Beluga: Programming with dependent types, contextual data, and contexts. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19\u201321, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6009, pp. 1\u201312. Springer (2010)","key":"459_CR52","DOI":"10.1007\/978-3-642-12251-4_1"},{"doi-asserted-by":"crossref","unstructured":"Pippenger, N.: Comparative schematology and pebbling with auxiliary pushdowns (preliminary version). In: Miller, R.E., Ginsburg, S., Burkhard, W.A., Lipton, R.J. (eds.) STOC. pp. 351\u2013356. ACM (1980)","key":"459_CR53","DOI":"10.1145\/800141.804684"},{"key":"459_CR54","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012787","volume-title":"Advances in Pebbling","author":"N Pippenger","year":"1982","unstructured":"Pippenger, N.: Advances in Pebbling. Springer, Berlin (1982)"},{"doi-asserted-by":"publisher","unstructured":"Reis, G.: Importing SMT and connection proofs as expansion trees. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2\u20133, 2015. EPTCS, vol. 186, pp. 3\u201310. doi: 10.4204\/EPTCS.186.3 (2015)","key":"459_CR55","DOI":"10.4204\/EPTCS.186.3"},{"issue":"1","key":"459_CR56","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"doi-asserted-by":"publisher","unstructured":"Rollini, S., Bruttomesso, R., Sharygina, N.: An efficient and flexible approach to resolution proof reduction. In: Hardware and Software: Verification and Testing\u20146th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4\u20137, 2010. Revised Selected Papers, pp. 182\u2013196. doi: 10.1007\/978-3-642-19583-9_17 (2010)","key":"459_CR57","DOI":"10.1007\/978-3-642-19583-9_17"},{"doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, C.: The twelf proof assistant. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17\u201320, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5674, pp. 79\u201383. Springer (2009)","key":"459_CR58","DOI":"10.1007\/978-3-642-03359-9_7"},{"issue":"3","key":"459_CR59","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1137\/0204020","volume":"4","author":"R Sethi","year":"1975","unstructured":"Sethi, R.: Complete register allocation problems. SIAM J. Comput. 4(3), 226\u2013248 (1975)","journal-title":"SIAM J. Comput."},{"unstructured":"Slaney, J., Paleo, B.W.: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning. CoRR abs\/1602.04568. http:\/\/arxiv.org\/abs\/1602.04568 (2016)","key":"459_CR60"},{"issue":"4","key":"459_CR61","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1016\/S0022-0000(73)80032-7","volume":"7","author":"SA Walker","year":"1973","unstructured":"Walker, S.A., Strong, H.R.: Characterizations of flowchartable recursions. J. Comput. Syst. Sci. 7(4), 404\u2013447 (1973)","journal-title":"J. Comput. Syst. Sci."},{"unstructured":"Woltzenlogel\u00a0Paleo, B.: Herbrand Sequent Extraction [M.Sc. Thesis]. VDM-Verlag, Saarbrucken, Germany (2008)","key":"459_CR62"},{"doi-asserted-by":"publisher","unstructured":"Woltzenlogel\u00a0Paleo, B.: Atomic cut introduction by resolution: proof structuring and compression. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning\u201416th International Conference, LPAR-16, Dakar, Senegal, April 25\u2013May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6355, pp. 463\u2013480. Springer. doi: 10.1007\/978-3-642-17511-4_26 (2010)","key":"459_CR63","DOI":"10.1007\/978-3-642-17511-4_26"},{"doi-asserted-by":"publisher","unstructured":"Woltzenlogel\u00a0Paleo, B.: Contextual natural deduction. In: Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6\u20138, 2013. Proceedings. pp. 372\u2013386. doi: 10.1007\/978-3-642-35722-0_27 (2013)","key":"459_CR64","DOI":"10.1007\/978-3-642-35722-0_27"},{"doi-asserted-by":"publisher","unstructured":"Woltzenlogel\u00a0Paleo, B.: Implementation and evaluation of contextual natural deduction for minimal logic. In: Perspectives of System Informatics\u201410th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24\u201327, 2015, Revised Selected Papers, pp. 314\u2013324. doi: 10.1007\/978-3-319-41579-6_24 (2015)","key":"459_CR65","DOI":"10.1007\/978-3-319-41579-6_24"},{"unstructured":"Woltzenlogel\u00a0Paleo, B., Delahaye, D.: All About Proofs, Proofs for All, Mathematical Logic and Foundations, vol.\u00a055. College Publications, London, UK. http:\/\/www.collegepublications.co.uk\/logic\/mlf\/?00023 (2015)","key":"459_CR66"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0459-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0459-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0459-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T02:26:24Z","timestamp":1750386384000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0459-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,27]]},"references-count":66,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["459"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0459-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2017,6,27]]},"assertion":[{"value":"27 June 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}