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

*To*: pvs-help@csl.sri.com*Subject*: Proof status of theorems in batch mode*From*: Makarand <makarand@ittc.ukans.edu>*Date*: Wed, 21 Jun 2000 16:12:19 -0500*Delivery-Date*: Wed Jun 21 14:12:25 2000*Organization*: ITTC*Sender*: makarand@stephens.ittc.ukans.edu

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 ----------------------------------------------------------

- Prev by Date:
**Re: pvs batch mode** - Next by Date:
**Re: Proof status of theorems in batch mode** - Prev by thread:
**Help!** - Next by thread:
**Re: Proof status of theorems in batch mode** - Index(es):