Reliable reconstruction of fine-grained proofs in a proof assistant

DOI10.1007/978-3-030-79876-5_26MaRDI QIDQ2055877

Mathias Fleury, Hans-Jörg Schurr, Martin Desharnais

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_26

zbMATH Keywords

proof assistants; automatic theorem provers; proof verification

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• Isabelle
• Isabelle/HOL
• SMT-LIB
• z3
• Sledgehammer
• veriT
• MaSh
• E Theorem Prover
• SMTCoq