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

*To*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>, "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Help proving two-dimensional inequality*From*: "MUNOZ, CESAR (LARC-D320)" <cesar.a.munoz@xxxxxxxx>*Date*: Wed, 11 Jul 2012 16:42:02 -0500*Accept-language*: en-US*Acceptlanguage*: en-US*Cc*:*In-reply-to*: <45351478-DBFF-4DFE-964D-156CFCE550AD@dependablecomputing.com>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*Thread-index*: Ac1frgJlxMIbdGgFRaae6z6BAOWXDw==*Thread-topic*: [PVS-Help] Help proving two-dimensional inequality*User-agent*: Microsoft-MacOutlook/14.12.0.110505

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 >

**Follow-Ups**:**Re: [PVS-Help] Help proving two-dimensional inequality***From:*Ben Hocking

**References**:**[PVS-Help] Help proving two-dimensional inequality***From:*Ben Hocking

- Prev by Date:
**[PVS-Help] Help proving two-dimensional inequality** - Next by Date:
**Re: [PVS-Help] Help proving two-dimensional inequality** - Previous by thread:
**[PVS-Help] Help proving two-dimensional inequality** - Next by thread:
**Re: [PVS-Help] Help proving two-dimensional inequality** - Index(es):