[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Format of the .prf files


is there any documentation about the format of PVS proof files?

If not, is it possible to document the grammar of the prf files?

Background: In our project [1] we develop a frontend for PVS. The
interface is simple, the frontend outputs files that one can
typecheck in PVS. We would like to let the frontend also generate
proofs for TCC's and lemmas. But how to do that?

For PVS versions 2.x and earlier the format of the prf files was
so simple that I guessed the grammar. I did not have it 100
percent right but it worked. 



[1] The VFiasco Project: http://www.vfiasco.org/