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

*To*: A Serebrenik <aserebre@xxxxxxxxxx>*Subject*: Re: [PVS-Help] inequalities in PVS*From*: Ben Di Vito <Benedetto.L.DiVito@xxxxxxxx>*Date*: Wed, 17 Oct 2007 16:59:38 -0400*Cc*: pvs-help@xxxxxxxxxxx*In-Reply-To*: <Pine.LNX.4.64.0710172137180.8228@pclin132>*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*: <Pine.LNX.4.64.0710172137180.8228@pclin132>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: Thunderbird 1.5 (X11/20060313)

Alexander, This problem and many like it can be solved using strategy packages that we've developed at NASA Langley and NIA. If you are a user of the NASA Langley libraries found at http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html you probably have the strategy packages Manip and Field already loaded. If not, you can retrieve the libraries or just the strategies from the web site. A proof of your conjecture is easy to obtain using these strategies, which were designed to help with cases requiring detailed manipulation such as yours. Learning to use them requires some investment of your time, of course, but if you expect to do a lot of proving, you would realize a benefit from the effort. So here is how it goes: {-1} x!1 < 1000 {-2} x!1 > 1 {-3} x!1 * x!1 > 1 {-4} x!1 * x!1 < 1000 |------- {1} 1000 - x!1 * x!1 < 1000 - x!1 Rerunning step: (field 1) both_sides_minus_lt2 rewrites 1000 - x!1 * x!1 < 1000 - x!1 to x!1 < x!1 * x!1 Simplifying formula 1 with FIELD, this simplifies to: m1 : [-1] x!1 < 1000 [-2] x!1 > 1 [-3] x!1 * x!1 > 1 [-4] x!1 * x!1 < 1000 |------- {1} x!1 < x!1 * x!1 Rerunning step: (op-ident 1 l) Applying identity operation to rewrite selected expression, this simplifies to: m1 : [-1] x!1 < 1000 [-2] x!1 > 1 [-3] x!1 * x!1 > 1 [-4] x!1 * x!1 < 1000 |------- {1} (x!1 * 1 < x!1 * x!1) Rerunning step: (cancel 1) Canceling terms from both sides of selected formulas, this simplifies to: m1 : [-1] x!1 < 1000 [-2] x!1 > 1 [-3] x!1 * x!1 > 1 [-4] x!1 * x!1 < 1000 |------- {1} 1 < x!1 Rerunning step: (assert) Simplifying, rewriting, and recording with decision procedures, Q.E.D. --------- The strategy "field" performs many reductions automatically, although it mostly helps when divisions are present. In this case it rearranges the conclusion the way we would like it. Next we want to cancel an "x" from both sides, but first we need to create a more symmetric formula to set up the cancellation. The strategy "op-ident" is the helper and "cancel" does what we need to eliminate the "x". The rest is handled by assert. Regards, Ben Di Vito 1 South Wright Street, MS 130 NASA Langley Research Center Hampton, VA 23681 USA voice: +1-757-864-4883 fax: +1-757-864-4234 b.divito@nasa.gov http://shemesh.larc.nasa.gov/people/bld --------- A Serebrenik wrote: > Dear all, > > I wonder what proof command should I use for simple manipulation of > inequalities? I would like, e.g. to prove the following sequent: > {-1} integer_pred(x!1) > {-2} x!1 < 1000 > {-3} x!1 > 1 > {-4} x!1 * x!1 > 1 > {-5} x!1 * x!1 < 1000 > |------- > {1} 1000 - x!1 * x!1 < 1000 - x!1 > > Using (both-sides - 1000) and (assert) I can reduce the succedent to > {1'} -1 * (x!1 * x!1) < -1 * x!1 but this is as far as I get: > (both-sides * -1) results in an unexpected: > {1''} -1 * (x!1 * x!1) * -1 < -1 * x!1 * -1 > > Best regards, > Alexander Serebrenik > >

**References**:**[PVS-Help] inequalities in PVS***From:*A Serebrenik

- Prev by Date:
**Re: [work] [PVS-Help] inequalities in PVS** - Next by Date:
**[PVS-Help] Sets-reaching their individual elements, Graphs** - Prev by thread:
**Re: [work] [PVS-Help] inequalities in PVS** - Next by thread:
**[PVS-Help] problem with the RANDOM function** - Index(es):