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

*To*: "MUNOZ, CESAR (LARC-D320)" <cesar.a.munoz@xxxxxxxx>*Subject*: Re: [PVS-Help] Help proving two-dimensional inequality*From*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Date*: Thu, 12 Jul 2012 07:48:31 -0400*Cc*: "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>*In-reply-to*: <CC236972.E69C%cesar.a.munoz@nasa.gov>*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>*References*: <CC236972.E69C%cesar.a.munoz@nasa.gov>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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 >> > >

**References**:**Re: [PVS-Help] Help proving two-dimensional inequality***From:*MUNOZ, CESAR (LARC-D320)

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