{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:01Z","timestamp":1776333421229,"version":"3.51.2"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030798758","type":"print"},{"value":"9783030798765","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a fast and reliable reconstruction of proofs generated by the SMT solver veriT in Isabelle. The fine-grained proof format makes the reconstruction simple and efficient. For typical proof steps, such as arithmetic reasoning and skolemization, our reconstruction can avoid expensive search. By skipping proof steps that are irrelevant for Isabelle, the performance of proof checking is improved. Our method increases the success rate of Sledgehammer by halving the failure rate and reduces the checking time by 13%. We provide a detailed evaluation of the reconstruction time for each rule. The runtime is influenced by both simple rules that appear very often and common complex rules.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_26","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"450-467","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0829-5056","authenticated-orcid":false,"given":"Hans-J\u00f6rg","family":"Schurr","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1705-3083","authenticated-orcid":false,"given":"Mathias","family":"Fleury","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1830-7532","authenticated-orcid":false,"given":"Martin","family":"Desharnais","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","unstructured":"Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant. Zenodo (Apr 2021). https:\/\/doi.org\/10.5281\/zenodo.4727349","DOI":"10.5281\/zenodo.4727349"},{"key":"26_CR2","unstructured":"Abdulaziz, M., Paulson, L.C.: An Isabelle\/HOL formalisation of Green\u2019s theorem. Archive of Formal Proofs (Jan 2018), https:\/\/isa-afp.org\/entries\/Green.html, formal proof development"},{"key":"26_CR3","doi-asserted-by":"publisher","unstructured":"Abdulaziz, M., Paulson, L.C.: An Isabelle\/HOL Formalisation of Green\u2019s Theorem. Journal of Automated Reasoning 63(3), 763\u2013786 (Nov 2018). https:\/\/doi.org\/10.1007\/s10817-018-9495-z","DOI":"10.1007\/s10817-018-9495-z"},{"key":"26_CR4","doi-asserted-by":"publisher","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 Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"26_CR5","unstructured":"Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., Saillard, R.: Expressing theories in the $$\\lambda $$$$\\pi $$-calculus modulo theory and in the Dedukti system. In: TYPES: Types for Proofs and Programs. Novi SAd, Serbia (May 2016)"},{"key":"26_CR6","unstructured":"Barbosa, H.: Efficient instantiation techniques in SMT (work in progress). vol. 1635, pp. 1\u201310. CEUR-WS.org (Jul 2016), http:\/\/ceur-ws.org\/Vol-1635\/#paper-01"},{"key":"26_CR7","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Blanchette, J.C., Fleury, M., Fontaine, P.: Scalable fine-grained proofs for formula processing. Journal of Automated Reasoning (Jan 2019). https:\/\/doi.org\/10.1007\/s10817-018-09502-y","DOI":"10.1007\/s10817-018-09502-y"},{"key":"26_CR8","doi-asserted-by":"publisher","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. Springer, Berlin Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_13","DOI":"10.1007\/978-3-662-54580-5_13"},{"key":"26_CR9","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) CADE 27. LNCS, vol. 11716, pp. 35\u201354. Springer International Publishing (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_3","DOI":"10.1007\/978-3-030-29436-6_3"},{"key":"26_CR10","doi-asserted-by":"publisher","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Berlin Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"26_CR11","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017), available at www.SMT-LIB.org"},{"key":"26_CR12","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of Knuth\u2013Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs (Nov 2016), https:\/\/isa-afp.org\/entries\/Lambda_Free_KBOs.html, formal proof development","DOI":"10.1007\/978-3-319-63046-5_27"},{"key":"26_CR14","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., B\u00f6hme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar Proofs from Machine-Generated Proofs. Journal of Automated Reasoning 56(2), 155\u2013200 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9335-3","DOI":"10.1007\/s10817-015-9335-3"},{"key":"26_CR15","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with smt solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 23. LNCS, vol. 6803, pp. 116\u2013130. Springer, Berlin Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_11","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"26_CR16","unstructured":"B\u00f6hme, S.: Proving Theorems of Higher-Order Logic with SMT Solvers. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2012), http:\/\/mediatum.ub.tum.de\/node?id=1084525"},{"key":"26_CR17","doi-asserted-by":"publisher","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. pp. 107\u2013121. Springer, Berlin Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_9","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"26_CR18","doi-asserted-by":"publisher","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Berlin Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"26_CR19","doi-asserted-by":"publisher","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 Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"26_CR20","doi-asserted-by":"publisher","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, J., Fitzgerald, J.A., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194\u2013207. Springer, Berlin Heidelberg (Jun 2012). https:\/\/doi.org\/10.1007\/978-3-642-30885-7_14","DOI":"10.1007\/978-3-642-30885-7_14"},{"key":"26_CR21","unstructured":"Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Tech. rep., SRI International (May 2006), http:\/\/www.csl.sri.com\/users\/bruno\/publis\/sri-csl-06-01.pdf"},{"key":"26_CR22","unstructured":"Eberl, M.: Elementary facts about the distribution of primes. Archive of Formal Proofs (Feb 2019), https:\/\/isa-afp.org\/entries\/Prime_Distribution_Elementary.html, formal proof development"},{"key":"26_CR23","unstructured":"Eberl, M., Paulson, L.C.: The prime number theorem. Archive of Formal Proofs (Sep 2018), https:\/\/isa-afp.org\/entries\/Prime_Number_Theorem.html, formal proof development"},{"key":"26_CR24","doi-asserted-by":"publisher","unstructured":"Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.W.: SMTCoq: A plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kuncak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 126\u2013133. Springer International Publishing (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"26_CR25","doi-asserted-by":"publisher","unstructured":"Fleury, M., Schurr, H.: Reconstructing veriT proofs in Isabelle\/HOL. In: Reis, G., Barbosa, H. (eds.) PxTP 2019. EPTCS, vol. 301, pp. 36\u201350 (2019). https:\/\/doi.org\/10.4204\/EPTCS.301.6","DOI":"10.4204\/EPTCS.301.6"},{"key":"26_CR26","doi-asserted-by":"publisher","unstructured":"Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09724-4","DOI":"10.1007\/3-540-09724-4"},{"key":"26_CR27","unstructured":"Immler, F.: Re: [isabelle] Isabelle 2019-RC2 sporadic smt failures. Email (May 2019), https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2019-May\/msg00130.html"},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: Machine learning for Sledgehammer. In: ITP. LNCS, vol. 7998, pp. 35\u201350. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_6"},{"key":"26_CR29","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 361\u2013381. Springer International Publishing (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_20","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"26_CR30","unstructured":"Mari\u0107, F., Spasi\u0107, M., Thiemann, R.: An incremental simplex algorithm with unsatisfiable core generation. Archive of Formal Proofs (Aug 2018), https:\/\/isa-afp.org\/entries\/Simplex.html, formal proof development"},{"key":"26_CR31","doi-asserted-by":"publisher","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. Electronic Notes in Theoretical Computer Science 144(2), 43\u201351 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.12.005","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"26_CR32","unstructured":"McMillan, K.L.: Interpolants from Z3 proofs. In: FMCAD 2011. pp. 19\u201327. FMCAD Inc, Austin, Texas (2011)"},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41\u201357 (2009)","DOI":"10.1016\/j.jal.2007.07.004"},{"key":"26_CR34","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Berlin Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"26_CR35","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 112\u2013131. Springer International Publishing (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_7","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"26_CR36","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: FMCAD 2014. pp. 195\u2013202. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987613","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"26_CR37","doi-asserted-by":"crossref","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalization of Bachmair and Ganzinger\u2019s ordered resolution prover. Archive of Formal Proofs (Jan 2018), https:\/\/isa-afp.org\/entries\/Ordered_Resolution_Prover.html, formal proof development","DOI":"10.29007\/pn71"},{"key":"26_CR38","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Communications 15(2\u20133), 111\u2013126 (2002), http:\/\/content.iospress.com\/articles\/ai-communications\/aic260"},{"key":"26_CR39","doi-asserted-by":"publisher","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods in System Design 42(1), 91\u2013118 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0163-3","DOI":"10.1007\/s10703-012-0163-3"},{"key":"26_CR40","unstructured":"The veriT Team and Contributors: Proofonomicon: A reference of the veriT proof format. Software Documentation (2021), https:\/\/www.verit-solver.org\/documentation\/proofonomicon.pdf, last Accessed: April 2021"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:33:24Z","timestamp":1625650404000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}