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, but a development version,

git clone github.com/gabrielhdt/lambdapi.git
git checkout 3ac05539d019206ab191c21c8b487e9fb0750aee
make
make install

Structure

• personoj: encoding of PVS into Dedukti
• personoj/extra: encodings that are not needed for PVS
• personoj/examples: examples of PVS development in Lambdapi
• sandbox: miscellaneous experiments

Dedukti coding conventions

• Dedukti types are capitalised
  Nat: TYPE
• Predicates are suffixed with _p
even_p: Nat → Prop
• Documentation is commented with ///