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

Re: [PVS-Help] Help proving two-dimensional inequality



Thanks, Cesar.

That not only solved this specific problem, but all of the other similar problems that it was based on.

Regards,
-Ben

On Jul 11, 2012, at 5:42 PM, MUNOZ, CESAR (LARC-D320) wrote:

> Ben,
> 
> This problem is non-linear, i.e., it involves a multiplications of two
> variables. For that reason, it is not solved by the strategies you tried.
> However, we have recently developed a strategy for automatically solving
> exactly these kinds of problems. It is available as part of the PVS NASA
> Libraries (see http://shemesh.larc.nasa.gov/people/cam/Bernstein).
> 
> The proof in PVS involves two steps: (skeep :preds? t), which introduces
> skolem constants with type information, and (bernstein), which is our
> strategy. The strategy bernstein doesn't depend on an oracle, I.e., there
> is an actual PVS proof that supports the Q.E.D.
> 
> Hope that this helps,
> 
> 
> Cesar
> 
> 
> oddly_specific_1a :
> 
>  |-------
> {1}   FORALL (x: {i: real | i >= 0 AND i < 4},
>              y: {i: real | i >= 2 AND i < 3}):
>        -21.1636 + 4.12282 * x + 17.23232 * y - 1.87144 * x * y > 0
> 
> 
> Rule? (skeep :preds? t)
> Skolemizing with the names of the bound variables,
> this simplifies to:
> oddly_specific_1a :
> 
> {-1}  x >= 0
> {-2}  x < 4
> {-3}  y >= 2
> {-4}  y < 3
>  |-------
> {1}   -21.1636 + 4.12282 * x + 17.23232 * y - 1.87144 * x * y > 0
> 
> Rule? (bernstein)
> [Bernstein] Proving polynomial inequality using Bernstein's basis,
> Q.E.D.
> 
> Run time  = 1.81 secs.
> Real time = 5.35 secs.
> 
> 
> 
> 
> -- 
> Cesar A. Munoz                             NASA Langley Research Center
> Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
> http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
> Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234
> 
> 
> 
> 
> On 7/11/12 3:27 PM, "Ben Hocking" <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>
> wrote:
> 
>> I have the following lemma I wish to prove:
>> oddly_specific_1a: LEMMA
>>  FORALL(x : {i : real | i >= 0 AND i < 4}, y : {i : real | i >= 2 AND i
>> < 3}):
>>    -21.1636 + 4.12282 * x + 17.23232 * y - 1.87144 * x * y > 0
>> Using (model-check) and (grind) get me no further than a
>> (skolem-typepred) would do.
>> 
>> In looking at some other inequality questions asked here, I tried
>> (grind-reals) and (grind :theories real_props) but both of those didn't
>> lead to what looked like useful transformations. I also tried a hail Mary
>> of adding "IMPORTING reals@top" to the top of my theory without luck.
>> 
>> I've plotted this in Grapher (Mac plotter program) and verified that it
>> is indeed true, but I suspect part of the problem might be that I
>> wouldn't know how to rigorously prove this using plain old
>> paper-and-pencil.
>> 
>> Any help in proving this via PVS would be appreciated.
>> 
>> -Ben
>> 
> 
>