[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
TCCs on inst?
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))
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