{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T13:19:00Z","timestamp":1774271940977,"version":"3.50.1"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T00:00:00Z","timestamp":1771804800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T00:00:00Z","timestamp":1771804800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-21- -CE25-0015-01"],"award-info":[{"award-number":["ANR-21- -CE25-0015-01"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-21- -CE25-0015-01"],"award-info":[{"award-number":["ANR-21- -CE25-0015-01"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-21- -CE25-0015-01"],"award-info":[{"award-number":["ANR-21- -CE25-0015-01"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2026,3]]},"DOI":"10.1007\/s00236-025-00515-w","type":"journal-article","created":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T12:27:53Z","timestamp":1771849673000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reconstruction of SMT proofs with Lambdapi"],"prefix":"10.1007","volume":"63","author":[{"given":"Alessio","family":"Coltellacci","sequence":"first","affiliation":[]},{"given":"Bruno","family":"Andreotti","sequence":"additional","affiliation":[]},{"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[]},{"given":"Gilles","family":"Dowek","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,2,23]]},"reference":[{"key":"515_CR1","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers (2009)","DOI":"10.1145\/1670412.1670413"},{"key":"515_CR2","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) First Intl. Conf. Interactive Theorem Proving (ITP 2010). LNCS, vol. 6172, pp. 179\u2013194. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"515_CR3","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-030-79876-5_26","volume-title":"Automated Deduction - CADE 28","author":"H-J Schurr","year":"2021","unstructured":"Schurr, H.-J., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28, pp. 450\u2013467. Springer, Cham (2021)"},{"key":"515_CR4","unstructured":"Hondet, G., Blanqui, F.: The New Rewriting Engine of Dedukti. In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 167, pp. 35\u201313516. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Paris, France (2020)"},{"key":"515_CR5","unstructured":"Dowek, G.: Deduction modulo theory. In: All About Proofs. Proofs for All., Wien, Austria (2014). https:\/\/inria.hal.science\/hal-01101829"},{"key":"515_CR6","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM 40, 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"515_CR7","doi-asserted-by":"crossref","unstructured":"Schurr, H.-J., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: Towards a Generic SMT Proof Format (extended abstract). In: PxTP 2021, pp. 49\u201354","DOI":"10.4204\/EPTCS.336.6"},{"key":"515_CR8","doi-asserted-by":"crossref","unstructured":"Bouton, T., Oliveira, D.C.B.D., D\u00e9harbe, D., Fontaine, P.: veriT: An open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) 22nd Intl. Conf. Automated Deduction (CADE-22). Lecture Notes in Computer Science, vol. 5663, pp. 151\u2013156. Springer, Montreal, Canada (2009)","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"515_CR9","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., et al.: Flexible proof production in an industrial-strength SMT solver. In: International Joint Conference on Automated Reasoning, pp. 15\u201335 (2022). Springer International Publishing Cham","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"515_CR10","doi-asserted-by":"publisher","unstructured":"Andreotti, B., Lachnitt, H., Barbosa, H.: Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format. In: Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, pp. 367\u2013386. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_19","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"515_CR11","doi-asserted-by":"crossref","unstructured":"Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: Fifth Annual IEEE Symp. Logic in Computer Science (LICS 1990), pp. 95\u2013105 (1990)","DOI":"10.1109\/LICS.1990.113737"},{"key":"515_CR12","doi-asserted-by":"crossref","unstructured":"Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA+ proofs. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) 18th Intl. Symp. Formal Methods (FM 2012). LNCS, vol. 7436, pp. 47\u2013154. Springer, Paris, France (2012)","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"515_CR13","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bj\u00f8rner, N.S., Sofronie-Stokkermans, V. (eds.) 23rd Intl. Conf. Automated Deduction (CADE-23). LNCS, vol. 6803, pp. 116\u2013130. Springer, Wroclaw, Poland (2011)","DOI":"10.1007\/978-3-642-22438-6_11"},{"issue":"1","key":"515_CR14","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"\u0141 Czajka","year":"2018","unstructured":"Czajka, \u0141, Kaliszyk, C.: Hammer for Coq: Automation for dependent type theory. J. Autom. Reason. 61(1), 423\u2013453 (2018)","journal-title":"J. Autom. Reason."},{"key":"515_CR15","first-page":"9","volume":"97","author":"L Czajka","year":"2018","unstructured":"Czajka, L.: A Shallow Embedding of Pure Type Systems into First-Order Logic. Types for Proofs and Programs (TYPES 2016). In: 22nd International Conference on Leibniz International Proceedings in Informatics (LIPIcs) 97, 9\u20131939 (2018)","journal-title":"In: 22nd International Conference on Leibniz International Proceedings in Informatics (LIPIcs)"},{"issue":"3","key":"515_CR16","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10817-018-09502-y","volume":"64","author":"H Barbosa","year":"2020","unstructured":"Barbosa, H., Blanchette, J.C., Fleury, M., Fontaine, P.: Scalable fine-grained proofs for formula processing. J. Autom. Reason. 64(3), 485\u2013510 (2020)","journal-title":"J. Autom. Reason."},{"key":"515_CR17","doi-asserted-by":"publisher","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Thery, L., Werner, B.: A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses. In: Jouannaud, Jean-Pierre, Shao, Zhong (eds.) First Intl. Conf. Certified Programs and Proofs (CPP 2011). LNCS, vol. 7086, pp. 135\u2013150. Springer, Lenting, Taiwan (2011).https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"515_CR18","doi-asserted-by":"crossref","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) Intl. Workshop Types for Proofs and Programs (TYPES 2006). LNCS, pp. 48\u201362. Springer, Berlin, Heidelberg (2006)","DOI":"10.1007\/978-3-540-74464-1_4"},{"key":"515_CR19","unstructured":"Hoenicke, J., Schindler, T.: A simple proof format for SMT. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories (IJCAR 2022) Part of the 8th Federated Logic Conference (FLoC 2022), August 11-12, 2022. CEUR Workshop Proceedings, vol. 3185, pp. 54\u201370. CEUR-WS.org, Haifa, Israel (2022)"},{"key":"515_CR20","unstructured":"Coltellacci, A., Merz, S., Dowek, G.: Reconstruction of SMT proofs with Lambdapi. In: Proc. 22nd Intl. Wsh. Satisfiability Modulo Theories Co-located with the 36th Intl. Conf. Computer Aided Verification (CAV 2024). CEUR Workshop Proceedings, vol. 3725, pp. 13\u201323. CEUR-WS.org, Montreal, Canada (2024)"},{"key":"515_CR21","unstructured":"Barbosa, H., Fleury, M., Fontaine, P., Schurr, H.-J.: The Alethe Proof Format An Evolving Specification and Reference. https:\/\/verit.gitlabpages.uliege.be\/alethe\/specification.pdf (2024)"},{"key":"515_CR22","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017\u20132024). Available at www.SMT-LIB.orghttps:\/\/smt-lib.org\/papers\/smt-lib-reference-v2.6-r2024-09-20.pdf"},{"key":"515_CR23","doi-asserted-by":"crossref","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the Lambda-Pi-Calculus Modulo. In: Typed Lambda Calculi and Applications, pp. 102\u2013117. Springer, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"515_CR24","first-page":"13","volume":"167","author":"F Blanqui","year":"2020","unstructured":"Blanqui, F.: Type Safety of Rewrite Rules in Dependent Types. Formal Structures for Computation and Deduction (FSCD 2020). In: 5th International Conference on Leibniz International Proceedings in Informatics (LIPIcs) 167, 13\u201311314 (2020)","journal-title":"In: 5th International Conference on Leibniz International Proceedings in Informatics (LIPIcs)"},{"key":"515_CR25","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory (1980)"},{"key":"515_CR26","unstructured":"Dowek, G.: On the definition of the classical connectives and quantifiers (2016)"},{"key":"515_CR27","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-71316-6_8","volume-title":"Programming Languages and Systems","author":"F Blanqui","year":"2007","unstructured":"Blanqui, F., Hardin, T., Weis, P.: On the implementation of construction functions for non-free concrete data types. In: De Nicola, R. (ed.) Programming Languages and Systems, pp. 95\u2013109. Springer, Berlin, Heidelberg (2007)"},{"key":"515_CR28","unstructured":"Blanqui, F.: Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Vol. 228, pp. 24\u201312414, (2022)"},{"key":"515_CR29","doi-asserted-by":"crossref","unstructured":"Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI - A confluence tool. In: Bj\u00f8rner, N.S., Sofronie-Stokkermans, V. (eds.) 23rd Intl. Conf. Automated Deduction (CADE-23). LNCS, vol. 6803, pp. 499\u2013505. Springer, Wroclaw, Poland (2011)","DOI":"10.1007\/978-3-642-22438-6_38"},{"key":"515_CR30","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Reconstructing fine-grained proofs of rewrites using a domain-specific language. In: FMCAD 2022, pp. 65\u201374 (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_12","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_12"},{"key":"515_CR31","doi-asserted-by":"publisher","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. In: LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013. LNCS, vol. 8312, pp. 274\u2013290. Springer, Berlin, Heidelberg (2013).https:\/\/doi.org\/10.1007\/978-3-642-45221-5_20","DOI":"10.1007\/978-3-642-45221-5_20"},{"key":"515_CR32","volume-title":"Specifying Systems","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems. Addison-Wesley, Boston, Mass (2002)"},{"key":"515_CR33","doi-asserted-by":"crossref","unstructured":"Merz, S., Vanzetto, H.: Automatic verification of TLA+ proof obligations with SMT solvers. In: 18th Intl. Conf. Logic for Programming, Artificial Intelligence, and Reasoning. LNCS, vol. 7180, pp. 289\u2013303. Springer, M\u00e9rida, Venezuela (2012)","DOI":"10.1007\/978-3-642-28717-6_23"},{"key":"515_CR34","doi-asserted-by":"crossref","unstructured":"Defourn\u00e9, R.: Encoding TLA+ proof obligations safely for SMT. In: 9th Intl. Conf. Rigorous State-Based Methods (ABZ 2023). LNCS, vol. 14010, pp. 88\u2013106. Springer, Nancy, France (2023)","DOI":"10.1007\/978-3-031-33163-3_7"},{"key":"515_CR35","doi-asserted-by":"crossref","unstructured":"Merz, S.: The specification language TLA+. In: Bj\u00f8rner, D., Henson, M.C. (eds.) Logics of Specification Languages. Monographs in Theoretical Computer Science, pp. 401\u2013451. Springer, Berlin-Heidelberg (2008)","DOI":"10.1007\/978-3-540-74107-7_8"},{"key":"515_CR36","unstructured":"Merz, S.: Termination detection in a ring. https:\/\/github.com\/tlaplus\/Examples\/tree\/master\/specifications\/ewd840"},{"key":"515_CR37","series-title":"Lecture Notes in Computer Science","first-page":"367","volume-title":"Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings","author":"A Coltellacci","year":"2025","unstructured":"Coltellacci, A., Merz, S.: Checking linear integer arithmetic proofs in lambdapi. In: Thiemann, R., Weidenbach, C. (eds.) Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings. Lecture Notes in Computer Science, vol. 15979, pp. 367\u2013385. Springer, Cham (2025)"},{"key":"515_CR38","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) Theoretical Aspects of Computer Software, Third International Symposium, TACS \u201997, Sendai, Japan, September 23-26, 1997, Proceedings. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (1997)"},{"key":"515_CR39","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: 18th Intl. Conf. Theorem Proving in Higher Order Logics (TPHOLs 2005). LNCS, vol. 3603. Springer, Oxford, UK (2005)","DOI":"10.1007\/11541868_7"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00515-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00515-w","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00515-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T12:25:45Z","timestamp":1774268745000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00515-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,23]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3]]}},"alternative-id":["515"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00515-w","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,23]]},"assertion":[{"value":"31 March 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 February 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"8"}}