Proof certificates in PVS

DOI10.1007/978-3-319-66107-0_17MaRDI QIDQ1687741zbMATH OpenOpenAlexFDO

Authors Frédéric Gilbert

Publication date 4 January 2018

Full work available at URL https://hal.inria.fr/hal-01673517/file/main.pdf

Mathematics Subject Classification ID

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

Recommendations

• The Proof Certifier Checkers
• A proposal for broad spectrum proof certificates
• Foundational proof certificates in first-order logic
• Translating between implicit and explicit versions of proof
• scientific article; zbMATH DE number 6741937

Cites work

• MetiTarski: An automatic theorem prover for real-valued special functions
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Describes a project that uses

Uses Software

• dedukti
• HOL Light
• ProofPower
• HOL
• TPTP
• PVS
• MetiTarski

This page was built for publication: Proof certificates in PVS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687741)