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

*To*: pvs-help@csl.sri.com*Subject*: TCCs on inst?*From*: Arons Tamarah <tamarah@wisdom.weizmann.ac.il>*Date*: Sun, 8 Nov 1998 17:06:35 +0200

Hi, Is there ant way to get PVS *ONLY* to instantiate fomrulae so as not to generate TCCs at all? I.e. If I have a sequent [-1] (FORALL a: f(a) IMPLIES g(a)) [-2] (FORALL b: k(b) IMPLIES m(b)) [-3] k(b!1) |------- [1] m(b!1) Where a and b are of incompatible types A and B. If I try to use (grind :if-match best) or (inst? :if-match best) PVS first instantiates -1 with b!1, generating unprovable TCCs. (In fact, this is a toy example and perhaps grind would work, but in general it does do the substitution so that I have unprobable TCCs). The only solution seems to be to actually specify the line number, when instantiating. However, this means doing all such proofs manually. I would really appreciate help with this as it is a recurring problem and prevents a lot of proofs from being automated. If there were a method to prevent all TCC-generating instantiations this would solve my problem entirely as all such instantiations are always incorrect. Thanks Tamarah

- Prev by Date:
**Auto-rewrites and instantiations** - Next by Date:
**Re: TCCs on inst?** - Prev by thread:
**Non-linearity** - Next by thread:
**Re: TCCs on inst?** - Index(es):