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

Re: [PVS-Help] Syntax and prover

Natarajan Shankar wrote:
> Robert:
>> 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?
> I'm not sure what you have in mind but there's no big downside to using IFF.
> The main difference between using = and IFF is that propositional commands
> like flatten, split, and prop process IFF but not =.  The rewrite
> commands handle both the same.  IFF could be inconvenient if you want
> to keep the equality in its undecomposed form.  

I was thinking about forward chaining.  Are IFFs suitable for forward
When I did the proofs by hand, I had to flatten antecedent IFFs into
implication pairs and work from there.  But I wasn't certain whether PVS
strategies would suffer from the same limitations as me!

Thanks for the help,

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