PVS proofs

Encodings of PVS and manual translations of PVS prelude and others. Use with lambdapi.

The work consists essentially in translating fragments of the PVS standard library, also known as Prelude. The prelude is available

• as raw PVS, https://raw.githubusercontent.com/SRI-CSL/PVS/master/lib/prelude.pvs;
• as a documentation in pdf, http://pvs.csl.sri.com/doc/pvs-prelude.pdf;
• as html, http://www.cs.rug.nl/~grl/ar06/prelude.html.

Requirements

lambdapi later than fda8752584af52cdc8158a7a80bbe7fce5720616

Structure

• adlib contains additional libraries not in the prelude
• encodings contains encodings of PVS into Dedukti, most of the work is done using cert_f encoding
• prelude contains parts of the PVS prelude
• sandbox contains miscellaneous experiments
• tools contains some additional scripts and utilities
• alternatives contains files in other encodings