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

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



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
>