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

[PVS-Help] Syntax and prover

I was wondering about connections between syntactic form of expressions
and their usability to PVS.  In particular:

1.  I may be doing something wrong, but my impression was that using IFF
expressions in proofs was less "convenient" (for lack of a better word).
 Is that true?  If so, would it be helpful for me to take IFF
expressions, and generate implication lemmas out of them for use in proofs?

2.  A relation I have been using is naturally expressed as a transition
relation of roughly the following form:

Trans(program, state, ancillary-state,program1, state1, ancillary-state1)

Question:  in order to do an inductive proof, should I group the three
state components into one entity (and then possibly provide a conversion
to get back the original form)?

Thank you,
Robert P. Goldman
Senior Scientist
Smart Information Flow Technologies (d/b/a SIFT, LLC)

211 N. First St., Suite 300
Minneapolis, MN 55401

Voice:	(612) 384-3454
Email:    rpgoldman@SIFT.info