18 citations · 18 across the 1 of their papers we have counts for
2 papers
cs.LO2021★ 18 cited
Alethe: Towards a Generic SMT Proof Format (extended abstract)
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa +1
The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are use…
cs.LO2019
Reconstructing veriT Proofs in Isabelle/HOL
Mathias Fleury, Hans-Jörg Schurr
Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness o…