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

PVS batch mode



Dear Sir,

To my understanding, PVS batch mode can automatically reprove the
theorems that have already been proved manually (i.e. with interaction),
but it cannot automatically prove new theorems that have never been
proved, right ?

I've generated hundreds of theorems using C/C++, and I want to use PVS
to prove them automatically (i.e. not first prove them with interaction
, and then rerun the proof).  How can I pass the theorems to PVS and
have them proved? I've read chapter 5 in the manual, but haven't found
the answers.

Your help is greatly appreciated. Thank you very much.

Yours sincerely,

Pu Zhang