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

*To*: pvs@csl.sri.com*Subject*: Re: Instantiation hints*From*: "Victor A. Carreno" <v.a.carreno@larc.nasa.gov>*Date*: Thu, 1 Feb 2001 10:22:48 -0500 (EST)*Cc*: pvs@csl.sri.com*Reply-To*: "Victor A. Carreno" <v.a.carreno@larc.nasa.gov>

c5: lemma (exists (a,b,c:real): a>b and b<c) => (exists (b,c,a:real): a<c and a<c) |------- {1} (EXISTS (a, b, c: real): a > b AND b < c) => (EXISTS (b, c, a: real): a < c AND a < c) Rule? (skosimp*) Repeatedly Skolemizing and flattening, this simplifies to: c5: {-1} a!1 > b!1 {-2} b!1 < c!1 |------- {1} (EXISTS (b, c, a: real): a < c AND a < c) Rule? (inst 1 "b!1" "c!1" "a!1") Instantiating the top quantifier in 1 with the terms: b!1, c!1, a!1, this simplifies to: c5: [-1] a!1 > b!1 [-2] b!1 < c!1 |------- {1} a!1 < c!1 AND a!1 < c!1 If you want to instantiate some and not others: {-1} a!1 > b!1 {-2} b!1 < c!1 |------- {1} (EXISTS (b, c, a: real): a < c AND a < c) Rule? (inst 1 "b!1" "_" "a!1") Instantiating the top quantifier in 1 with the terms: b!1, _, a!1, this simplifies to: c5: [-1] a!1 > b!1 [-2] b!1 < c!1 |------- {1} EXISTS (c): a!1 < c AND a!1 < c

- Prev by Date:
**Instantiation hints** - Next by Date:
**Instantiations** - Prev by thread:
**Re: Instantiation hints** - Next by thread:
**Instantiations** - Index(es):