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

*To*: pvs@csl.sri.com*Subject*: Instantiation hints*From*: Kellom{ki Pertti <pk@cs.tut.fi>*Date*: Thu, 1 Feb 2001 08:33:10 +0200 (EET)

I have to prove a number of theorems of the form (exists(a,b,c,...) : P(a,b,c,...)) => (exists(a,b,c,...) : Q(a,b,c,...)) where P=>Q is trivial once I get rid of the quantifications. The order of the quantified variables may not be the same in the two quantifications, but they have the same variables. Is there a way to tell PVS that it should instantiate "a" with "a!1", "b" with "b!1" etc.? -- Pertti

**Follow-Ups**:**Re: Instantiation hints***From:*Sam Owre <owre@csl.sri.com>

- Prev by Date:
**IMPORTING in PVS** - Next by Date:
**Re: Instantiation hints** - Prev by thread:
**IMPORTING in PVS** - Next by thread:
**Re: Instantiation hints** - Index(es):