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

Proof status of theorems in batch mode



 HI,
I am looking for a function that tells me the status of a 
theorem (whether proved or not). i.e. given a PVS theory:

A_theory: THEORY
BEGIN
F1: Theorem P(x)
F2: Theorem Q(x)
End A_theory

I prove F1 and F2 using my proof strategies and now i need to know if
they succeeded.
I need to do this from within a lisp function of my own
as i am running pvs in batch.

The functions like (STATUS-PVS-FILE) or (STATUS-PROOF-THEORY)
don't help much because i need to interpret (and not just display)
the proof status's of the theorems in my theory. is there a way to write
these buffers
into some file which i can then read again to interpret the proof
status. Surely there is an easier way.
I was looking at (PROVED? FDECL) and (UNPROVED? FDECL) which serve my
prupose,
but then i had trouble getting the right argument.
what and how can i access FDECL? 

Note:- This is all in PVS batch mode so i need a solution that
is noninteractive.
Thanks again.

**********************************************************
                   Makarand Patil
               System Level Design Group
                Call:- (785) 864 3041
----------------------------------------------------------