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

Re: TCCs on inst?




Tamarah:
 Discarding instantiations with TCCs sounds like a reasonable
request.  It'll require adding a flag to the inst? command.
I will look into it and get back to you.

-Shankar

> 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
> 
>