Home My Page Projects pvs-with-proofs
Summary Activity SCM

Project Members
Project Information

This project has not yet categorized itself in the Trove Software Map Registered: 2017-04-20 09:58
Public Tools
SCM Repository (Git: 3 updates, 32 adds)
Project description

The purpose of this work is to allow the proof system PVS to export proof certificates that can be checked externally. This is done through the instrumentation of PVS to record detailed proofs step by step during the proof search process. At the current stage of this work, proofs can be built for any PVS theory. However, some reasoning steps rely on unverified assumptions. For a restricted fragment of PVS, the proofs are exported to the universal proof checker Dedukti, and the unverified assumptions are proved externally using the automated theorem prover MetiTarski.