[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Syntax and prover
Natarajan Shankar wrote:
>> 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
Smart Information Flow Technologies (d/b/a SIFT, LLC)
211 N. First St., Suite 300
Minneapolis, MN 55401
Voice: (612) 384-3454