Proof certificates in PVS

DOI10.1007/978-3-319-66107-0_17zbMath1483.68482OpenAlexW2745567114MaRDI QIDQ1687741

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)

Uses Software

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

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

This page was built for publication: Proof certificates in PVS