{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T00:10:35Z","timestamp":1771891835634,"version":"3.50.1"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T00:00:00Z","timestamp":1546560000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,3]]},"DOI":"10.1007\/s10817-018-09502-y","type":"journal-article","created":{"date-parts":[[2019,1,3]],"date-time":"2019-01-03T21:04:55Z","timestamp":1546549495000},"page":"485-510","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Scalable Fine-Grained Proofs for Formula Processing"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0188-2300","authenticated-orcid":false,"given":"Haniel","family":"Barbosa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8367-0936","authenticated-orcid":false,"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1705-3083","authenticated-orcid":false,"given":"Mathias","family":"Fleury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4700-6031","authenticated-orcid":false,"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,4]]},"reference":[{"key":"9502_CR1","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-662-54580-5_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Haniel Barbosa","year":"2017","unstructured":"Barbosa, H., Fontaine, P., Reynolds, A.: Congruence closure with free variables. In: Legay, A., Margaria, T. (eds.) TACAS 2017, LNCS, vol. 10206, pp. 214\u2013230 (2017)"},{"key":"9502_CR2","unstructured":"Besson, F., Fontaine, P., Th\u00e9ry, L.: A flexible proof format for SMT: a proposal. In: Fontaine, P., Stump, A. (eds.) PxTP 2011, pp. 15\u201326 (2011)"},{"key":"9502_CR3","first-page":"135","volume-title":"CPP 2011, LNCS","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) CPP 2011, LNCS, vol. 7086, pp. 135\u2013150. Springer, Berlin (2011)"},{"issue":"2","key":"9502_CR4","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-015-9335-3","volume":"56","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., B\u00f6hme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. 56(2), 155\u2013200 (2016)","journal-title":"J. Autom. Reason."},{"key":"9502_CR5","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-319-40229-1_20","volume-title":"Automated Reasoning","author":"Gabriel Ebner","year":"2016","unstructured":"Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 293\u2013301. Springer, Berlin (2016)"},{"key":"9502_CR6","first-page":"179","volume-title":"ITP 2010, LNCS","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L. (eds.) ITP 2010, LNCS, vol. 6172, pp. 179\u2013194. Springer, Berlin (2010)"},{"key":"9502_CR7","volume-title":"CADE-26, LNCS","author":"H Barbosa","year":"2017","unstructured":"Barbosa, H., Blanchette, J.C., Fontaine, P.: Scalable fine-grained proofs for formula processing. In: de Moura, L. (ed.) CADE-26, LNCS. Springer, Berlin (2017)"},{"key":"9502_CR8","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical Report, University of Iowa (2015). \nhttp:\/\/smt-lib.org\/"},{"key":"9502_CR9","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28717-6_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Geoff Sutcliffe","year":"2012","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18, LNCS, vol. 7180, pp. 406\u2013419. Springer, Berlin (2012)"},{"key":"9502_CR10","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"issue":"1\u20132","key":"9502_CR11","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1016\/j.ic.2004.10.011","volume":"199","author":"H Nivelle de","year":"2005","unstructured":"de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Inf. Comput. 199(1\u20132), 24\u201354 (2005)","journal-title":"Inf. Comput."},{"key":"9502_CR12","first-page":"232","volume-title":"TPHOLs 2007, LNCS","author":"LC Paulson","year":"2007","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007, LNCS, vol. 4732, pp. 232\u2013245. Springer, Berlin (2007)"},{"key":"9502_CR13","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1016\/B978-044450813-3\/50008-4","volume-title":"Handbook of Automated Reasoning","author":"A Nonnengart","year":"2001","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 335\u2013367. Elsevier, Amsterdam (2001)"},{"key":"9502_CR14","first-page":"23","volume-title":"All About Proofs, Proofs for All, Mathematical Logic and Foundations","author":"C Barrett","year":"2015","unstructured":"Barrett, C., de Moura, L., Fontaine, P.: Proofs in satisfiability modulo theories. In: Woltzenlogel Paleo, B., Delahaye, D. (eds.) All About Proofs, Proofs for All, Mathematical Logic and Foundations, vol. 55, pp. 23\u201344. College Publications, New York (2015)"},{"key":"9502_CR15","first-page":"222","volume-title":"CADE-23, LNCS","author":"D D\u00e9harbe","year":"2011","unstructured":"D\u00e9harbe, D., Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploiting symmetry in SMT problems. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE-23, LNCS, vol. 6803, pp. 222\u2013236. Springer, Berlin (2011)"},{"key":"9502_CR16","first-page":"151","volume-title":"CADE-22, LNCS","author":"T Bouton","year":"2009","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-22, LNCS, vol. 5663, pp. 151\u2013156. Springer, Berlin (2009)"},{"key":"9502_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-order Logic, LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-order Logic, LNCS, vol. 2283. Springer, Berlin (2002)"},{"key":"9502_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation, LNCS","author":"MJC Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol. 78. Springer, Berlin (1979)"},{"key":"9502_CR19","unstructured":"B\u00f6hme, S.: Proving theorems of higher-order logic with SMT solvers. Ph.D. Thesis, Technische Universit\u00e4t M\u00fcnchen (2012)"},{"key":"9502_CR20","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/B978-044450813-3\/50007-2","volume-title":"Handbook of Automated Reasoning","author":"M Baaz","year":"2001","unstructured":"Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 273\u2013333. Elsevier, Amsterdam (2001)"},{"key":"9502_CR21","unstructured":"Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: Benzm\u00fcller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016, EPiC Series in Computing, vol. 41, pp. 11\u201323. EasyChair (2016)"},{"key":"9502_CR22","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: Benzm\u00fcller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016, EPiC Series in Computing, vol. 41, pp. 53\u201371. EasyChair (2016)"},{"key":"9502_CR23","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications, vol. 112, pp. 201\u2013215. IOS Press, Amsterdam (2004)"},{"key":"9502_CR24","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A., (eds.) LPAR-19, LNCS, vol. 8312, pp. 735\u2013743. Springer, Berlin (2013)"},{"key":"9502_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"Laura Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013, LNCS, vol. 8044, pp. 1\u201335. Springer, Berlin (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"9502_CR26","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"Christoph Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22, LNCS, vol. 5663, pp. 140\u2013145. Springer, Berlin (2009)"},{"key":"9502_CR27","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR 2008 Workshops, CEUR Workshop Proceedings, vol. 418. CEUR-WS.org (2008)"},{"key":"9502_CR28","unstructured":"Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. In: LICS\u201987, pp. 194\u2013204. IEEE Computer Society (1987)"},{"key":"9502_CR29","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/j.entcs.2008.12.121","volume":"228","author":"A Stump","year":"2009","unstructured":"Stump, A.: Proof checking technology for satisfiability modulo theories. Electron. Notes Theor. Comput. Sci. 228, 121\u2013133 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9502_CR30","first-page":"93","volume-title":"FMCAD 2016","author":"G Katz","year":"2016","unstructured":"Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.) FMCAD 2016, pp. 93\u2013100. IEEE Computer Society, New York (2016)"},{"key":"9502_CR31","first-page":"340","volume-title":"LPAR-20, LNCS","author":"L Hadarean","year":"2015","unstructured":"Hadarean, L., Barrett, C.W., Reynolds, A., Tinelli, C., Deters, M.: Fine grained SMT proofs for the theory of fixed-width bit-vectors. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20, LNCS, vol. 9450, pp. 340\u2013355. Springer, Berlin (2015)"},{"key":"9502_CR32","doi-asserted-by":"crossref","unstructured":"Moskal, M.: Rocket-fast proof checking for SMT solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 486\u2013500. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_38"},{"issue":"1835","key":"9502_CR33","doi-asserted-by":"publisher","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","volume":"363","author":"H Barendregt","year":"2005","unstructured":"Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Philos. Trans. R. Soc. Lond. Ser. A 363(1835), 2351\u20132375 (2005)","journal-title":"Philos. Trans. R. Soc. Lond. Ser. A"},{"key":"9502_CR34","first-page":"38","volume-title":"TPHOLs 2000, LNCS","author":"S Berghofer","year":"2000","unstructured":"Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000, LNCS, vol. 1869, pp. 38\u201352. Springer, Berlin (2000)"},{"key":"9502_CR35","first-page":"102","volume-title":"TLCA 2007, LNCS","author":"D Cousineau","year":"2007","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-Pi-calculus modulo. In: Rocca, S.R.D. (ed.) TLCA 2007, LNCS, vol. 4583, pp. 102\u2013117. Springer, Berlin (2007)"},{"issue":"1","key":"9502_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1182613.1182614","volume":"8","author":"A Guglielmi","year":"2007","unstructured":"Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Log. 8(1), 1 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"9502_CR37","first-page":"149","volume-title":"TABLEAUX 2013, LNCS","author":"S Graham-Lengrand","year":"2013","unstructured":"Graham-Lengrand, S.: Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013, LNCS, vol. 8123, pp. 149\u2013156. Springer, Berlin (2013)"},{"issue":"2","key":"9502_CR38","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"LC Paulson","year":"1983","unstructured":"Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119\u2013149 (1983)","journal-title":"Sci. Comput. Program."},{"key":"9502_CR39","doi-asserted-by":"crossref","unstructured":"Meier, A.: Tramp: transformation of machine-found proofs into natural deduction proofs at the assertion level (system description). In: McAllester, D. (ed.) CADE-17, LNCS, vol. 1831, pp. 460\u2013464. Springer, Berlin (2000)","DOI":"10.1007\/10721959_37"},{"key":"9502_CR40","first-page":"584","volume-title":"CSL 2002, LNCS","author":"H Nivelle de","year":"2002","unstructured":"de Nivelle, H.: Extraction of proofs from the clausal normal form transformation. In: Bradfield, J.C. (ed.) CSL 2002, LNCS, vol. 2471, pp. 584\u2013598. Springer, Berlin (2002)"},{"issue":"2","key":"9502_CR41","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2005.12.005","volume":"144","author":"S McLaughlin","year":"2006","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: a case study combining HOL-light and CVC lite. Electron. Notes Theor. Comput. Sci. 144(2), 43\u201351 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9502_CR42","first-page":"167","volume-title":"TACAS 2006, LNCS","author":"P Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006, LNCS, vol. 3920, pp. 167\u2013181. Springer, Berlin (2006)"},{"key":"9502_CR43","first-page":"183","volume-title":"CPP 2011, LNCS","author":"S B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3\u2019s bit-vector proofs in HOL4 and Isabelle\/HOL. In: Jouannaud, J., Shao, Z. (eds.) CPP 2011, LNCS, vol. 7086, pp. 183\u2013198. Springer, Berlin (2011)"},{"key":"9502_CR44","doi-asserted-by":"publisher","first-page":"21","DOI":"10.4204\/EPTCS.210.5","volume":"210","author":"Burak Ekici","year":"2016","unstructured":"Ekici, B., Katz, G., Keller, C., Mebsout, A., Reynolds, A.J., Tinelli, C.: Extending SMTCoq, a certified checker for SMT (extended abstract). In: Blanchette, J.C., Kaliszyk, C. (eds.) HaTT 2016, EPTCS, vol. 210, pp. 21\u201329 (2016)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9502_CR45","unstructured":"Zimmer, J., Meier, A., Sutcliffe, G., Zhan, Y.: Integrated proof transformation services. In: Benzm\u00fcller, C., Windsteiger, W. (eds.) IJCAR WS 7 (2004)"},{"key":"9502_CR46","first-page":"157","volume-title":"TABLEAUX 2013, LNCS","author":"S Hetzl","year":"2013","unstructured":"Hetzl, S., Libal, T., Riener, M., Rukhaia, M.: Understanding resolution proofs through Herbrand\u2019s theorem. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013, LNCS, vol. 8123, pp. 157\u2013171. Springer, Berlin (2013)"},{"key":"9502_CR47","unstructured":"Burel, G.: A shallow embedding of resolution and superposition proofs into the \n$$\\lambda \\Pi $$\n\n\n\n\n\u03bb\n\u03a0\n\n\n\n\n-calculus modulo. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EPiC Series in Computing, vol. 14, pp. 43\u201357. EasyChair (2013)"},{"key":"9502_CR48","first-page":"3","volume-title":"LOPSTR 2015, LNCS","author":"D Miller","year":"2015","unstructured":"Miller, D.: Proof checking and logic programming. In: Falaschi, M. (ed.) LOPSTR 2015, LNCS, vol. 9527, pp. 3\u201317. Springer, Berlin (2015)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-09502-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-09502-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-09502-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,29]],"date-time":"2020-02-29T04:03:10Z","timestamp":1582948990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-09502-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,4]]},"references-count":48,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["9502"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-09502-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,4]]},"assertion":[{"value":"30 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 November 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 January 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}