Reconstructing veriT Proofs in Isabelle/HOL

Fleury, Mathias; Schurr, Hans-Jörg

doi:10.4204/EPTCS.301.6

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

学術論文

Reconstructing veriT Proofs in Isabelle/HOL

MPS-Authors

/persons/resource/persons141910

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

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

arXiv:1908.09480.pdf
(プレプリント), 216KB

付随資料 (公開)

There is no public supplementary material available

引用

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.

引用: https://hdl.handle.net/21.11116/0000-0005-8879-A

要旨

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.