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

Re: Instantiation hints

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