Reconstructing veriT Proofs in Isabelle/HOL

Reconstructing veriT Proofs in Isabelle/HOL

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...

Full description

Bibliographic Details
Main Authors: Mathias Fleury, Hans-Jörg Schurr
Format: Article
Language:English
Published: Open Publishing Association 2019-08-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1908.09480v1
id doaj-d9fc61abda5244708dced3e614a74afb
record_format Article
spelling doaj-d9fc61abda5244708dced3e614a74afb2020-11-25T02:43:14ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-08-01301Proc. PxTP 2019365010.4204/EPTCS.301.6:7Reconstructing veriT Proofs in Isabelle/HOLMathias Fleury0Hans-Jörg Schurr1 Max Planck Institut for Informatics University of Lorraine, CNRS, Inria, and LORIA 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.http://arxiv.org/pdf/1908.09480v1
collection DOAJ
language English
format Article
sources DOAJ
author Mathias Fleury
Hans-Jörg Schurr
spellingShingle Mathias Fleury
Hans-Jörg Schurr
Reconstructing veriT Proofs in Isabelle/HOL
Electronic Proceedings in Theoretical Computer Science
author_facet Mathias Fleury
Hans-Jörg Schurr
author_sort Mathias Fleury
title Reconstructing veriT Proofs in Isabelle/HOL
title_short Reconstructing veriT Proofs in Isabelle/HOL
title_full Reconstructing veriT Proofs in Isabelle/HOL
title_fullStr Reconstructing veriT Proofs in Isabelle/HOL
title_full_unstemmed Reconstructing veriT Proofs in Isabelle/HOL
title_sort reconstructing verit proofs in isabelle/hol
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2019-08-01
description 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.
url http://arxiv.org/pdf/1908.09480v1
work_keys_str_mv AT mathiasfleury reconstructingveritproofsinisabellehol
AT hansjorgschurr reconstructingveritproofsinisabellehol
_version_ 1724770676319977472

Similar Items