TCCs on inst?

[Arons Tamarah <tamarah@wisdom.weizmann.ac.il>]

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):
  • Date
  • Thread