English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse
  1. Tools / 
  2. View item / 
  3. Item Summary

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Journal Article

Reconstructing veriT Proofs in Isabelle/HOL

MPS-Authors
/persons/resource/persons141910

Fleury,  Mathias
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

arXiv:1908.09480.pdf
(Preprint), 216KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Fleury, M., & Schurr, H.-J. (2019). Reconstructing veriT Proofs in Isabelle/HOL. Electronic Proceedings in Theoretical Computer Science, (301), 36-50. doi:10.4204/EPTCS.301.6.


Cite as: https://hdl.handle.net/21.11116/0000-0005-8879-A
Abstract
Automated theorem provers are now commonly used within interactive theorem
provers to discharge an increasingly large number of proof obligations. To
maintain the trustworthiness of a proof, the automatically found proof must be
verified inside the proof assistant. We present here a reconstruction procedure
in the proof assistant Isabelle/HOL for proofs generated by the satisfiability
modulo theories solver veriT which is part of the smt tactic. We describe in
detail the architecture of our improved reconstruction method and the
challenges we faced in designing it. Our experiments show that the
veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest
method to automatically solve proof goals.