Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

Conference proceeding

Hanna Lachnitt, Haniel Barbosa, Bruno Andreotti, Hans Jörg Schurr, Cesare Tinelli, Mathias Fleury, Jibiana Jakpor, Andrew Reynolds and Clark Barrett

16th International Conference on Interactive Theorem Proving, ITP 2025, Vol.352, 26

09/22/2025

DOI: 10.4230/LIPIcs.ITP.2025.26

Files and links (1)

url

https://doi.org/10.4230/lipics.itp.2025.26View

Open Access

certification

interactive theorem proving

Isabelle/HOL

proof assistants

proof automation

proof certificates

proof reconstruction

SMT

Title: Subtitle: Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL
Creators: Hanna Lachnitt - Stanford University
Haniel Barbosa - Universidade Federal de Minas Gerais
Bruno Andreotti - Universidade Federal de Minas Gerais
Hans Jörg Schurr - University of Iowa, Computer Science
Cesare Tinelli - University of Iowa
Mathias Fleury - University of Freiburg
Jibiana Jakpor - Stanford University
Andrew Reynolds - University of Iowa, Computer Science
Clark Barrett - Stanford University
Resource Type: Conference proceeding
Publication Details: 16th International Conference on Interactive Theorem Proving, ITP 2025, Vol.352, 26
DOI: 10.4230/LIPIcs.ITP.2025.26
ISSN: 1868-8969
Grant note: Intel Corporation (http://data.elsevier.com/vocabulary/SciValFunders/100002418) FA8750-24-2-1001 / Defense Advanced Research Projects Agency (http://data.elsevier.com/vocabulary/SciValFunders/100000185) Defense Advanced Research Projects Agency (http://data.elsevier.com/vocabulary/SciValFunders/100000185)
Language: English
Date published: 09/22/2025
Academic Unit: Computer Science
Record Identifier: 9985024249202771

36 Record Views