[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)?
Robert P. Goldman
Smart Information Flow Technologies (d/b/a SIFT, LLC)
211 N. First St., Suite 300
Minneapolis, MN 55401
Voice: (612) 384-3454