Search Results

Documents authored by Lachnitt, Hanna

Artifact
Software
DOI: 10.4230/artifacts.27121
Apply2Isar

Authors: Sage Binder, Hanna Lachnitt, and Katherine Kosaian

Abstract
Cite as

Sage Binder, Hanna Lachnitt, Katherine Kosaian. Apply2Isar (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27121,
   title = {{Apply2Isar}}, 
   author = {Binder, Sage and Lachnitt, Hanna and Kosaian, Katherine},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:8753f0c693cdc7159375110e6dd9d977e62984a8;origin=https://github.com/sagebinder/apply2isar;visit=swh:1:snp:d413b506ca05f076c64c1ed2cf58f8c55da2f875;anchor=swh:1:rev:ecca6ce39f971746f0f3e35caf20e818819079d0}{\texttt{swh:1:dir:8753f0c693cdc7159375110e6dd9d977e62984a8}} (visited on 2026-07-16)},
   url = {https://github.com/sagebinder/apply2isar},
   doi = {10.4230/artifacts.27121},
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.18
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

Authors: Sage Binder, Hanna Lachnitt, and Katherine Kosaian

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proofs since they enable rapid exploration of the search space. To get the best of both worlds, we introduce Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style proofs to declarative Isar. This allows users to write complex, possibly fragile apply-style proofs, and then automatically convert them to more readable and robust declarative Isar proofs. To demonstrate the efficacy of Apply2Isar in practice, we evaluate it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.
Cite as

Sage Binder, Hanna Lachnitt, and Katherine Kosaian. Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{binder_et_al:LIPIcs.ITP.2026.18,
  author =	{Binder, Sage and Lachnitt, Hanna and Kosaian, Katherine},
  title =	{{Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.18},
  URN =		{urn:nbn:de:0030-drops-269925},
  doi =		{10.4230/LIPIcs.ITP.2026.18},
  annote =	{Keywords: Proof Assistants, Isabelle/HOL, Isabelle/ML, Isabelle/Isar, Proof Refactoring}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.26
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

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

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Sledgehammer is a tool that increases the level of automation in the Isabelle/HOL proof assistant by asking external automatic theorem provers (ATPs), including SMT solvers, to prove the current goal. When the external ATP succeeds it must provide enough evidence that the goal holds for Isabelle to be able to reprove it internally based on that evidence. In particular, Isabelle can do this by replaying fine-grained proof certificates from proof-producing SMT solvers as long as they are expressed in the Alethe format, which until now was supported only by the veriT SMT solver. We report on our experience adding proof reconstruction support for the cvc5 SMT solver in Isabelle by extending cvc5 to produce proofs in the Alethe format and then adapting Isabelle to reconstruct those proofs. We discuss several difficulties and pitfalls we encountered and describe a set of tools and techniques we developed to improve the process. A notable outcome of this effort is that Isabelle can now be used as an independent proof checker for SMT problems written in the SMT-LIB standard. We evaluate cvc5’s integration on a set of SMT-LIB benchmarks originating from Isabelle as well as on a set of Isabelle proofs. Our results confirm that this integration complements and improves Sledgehammer’s capabilities.
Cite as

Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lachnitt_et_al:LIPIcs.ITP.2025.26,
  author =	{Lachnitt, Hanna and Fleury, Mathias and Barbosa, Haniel and Jakpor, Jibiana and Andreotti, Bruno and Reynolds, Andrew and Schurr, Hans-J\"{o}rg and Barrett, Clark and Tinelli, Cesare},
  title =	{{Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.26},
  URN =		{urn:nbn:de:0030-drops-246243},
  doi =		{10.4230/LIPIcs.ITP.2025.26},
  annote =	{Keywords: interactive theorem proving, proof assistants, Isabelle/HOL, SMT, certification, proof certificates, proof reconstruction, proof automation}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact