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

*To*: Michel Levy <Michel.Levy@imag.fr>*Subject*: Re: seeking proof of a trivial fact*From*: John Rushby <rushby@csl.sri.com>*Date*: Sat, 13 Jul 2002 11:47:19 PDT*Cc*: pvs-help@csl.sri.com*In-Reply-To*: Your message of Sat, 13 Jul 2002 19:52:28 +0200*Sender*: pvs-help-owner@csl.sri.com

> b41 : lemma forall (x, y: real): x >=0 and y <= 1 > => x * y <= x > Why this lemma is not trivial in PVS ? Because it involves nonlinear arithmetic, which is not decided in PVS (and, in its full generality, is undecidable in combination with the other theories decided by PVS). To prove it, you need to invoke the lemmas in the prelude theory real_props. For example, the following does it. (SKOSIMP) (LEMMA "both_sides_times_pos_ge1") (INST - "x!1" "1" "y!1") (("1" (ASSERT)) ("2" (ASSERT))) You might want to investigate the NASA field and manip strategy packages, which are designed precisely to ease these difficulties. See http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html Lack of automation for nonlinear arithmetic is one of the biggest complaints we receive about PVS, and we working to improve the way it is handled by the decision procedures. John Rushby

- Prev by Date:
**seeking proof of a trivial fact** - Next by Date:
**Re: seeking proof of a trivial fact** - Prev by thread:
**seeking proof of a trivial fact** - Next by thread:
**Re: seeking proof of a trivial fact** - Index(es):