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

*To*: pvs-help@csl.sri.com*Subject*: Re: Proofing problem*From*: Holger Pfeifer <pfeifer@ares.informatik.uni-ulm.de>*Date*: Wed, 20 Feb 2002 10:58:35 +0100*References*: <Pine.GHP.4.32.0202191144580.16038-100000@stud3.tuwien.ac.at>*Sender*: pvs-help-owner@csl.sri.com

Wilfried, > My problem is, PVS wants me to proof: > > {-1} interval > 0 > {-2} interval <= max_interval > [-3] number_intervals > 0 > [-4] p!1 >= 0 > [-5] p!1 < number_intervals > |------- > [1] interval * number_intervals > p!1 * interval - interval > > where interval and number_intervals are of type nat. On paper, you would complete your proof by first rewriting the right hand side of [1] to "interval * (p!1 - 1)" followed by cancelling the factor "interval" on both sides (bearing in mind that "interval" is non-zero, by [-1]). The remaining goal "number_intervals > p!1 - 1" then follows directly from [-5]. To follow this outline with PVS, you need to apply appropriate lemmas. Fortunately, PVS comes with a large 'prelude', which contains various useful proved facts. The key to your problem is found in the theory 'real_props'. Use the Emacs-command "M-x view-prelude-theory" to have a look at it. Among various other things, you can find the lemma both_sides_times_neg_gt2: LEMMA nz * x > nz * y IFF y > x which captures the cancellation step mentioned above. You can accomplish the preceding rewriting step either explicitly, by using the command (CASE-REPLACE "p!1 * interval - interval = interval * (p!1 - 1)") or implicitly by using an appropriate instance of the lemma above, such as: (USE "both_sides_times_pos_gt2" :SUBST ("pz" "interval" "y" "p!1-1")) In each case, the remaining goals are solved by PVS's ground prover (GROUND). Regards, - Holger PS.: If you need to do these kind of proofs more often, you might want to have a look at Ben Di Vito's "Manip" package (http://shemesh.larc.nasa.gov/people/bld/manip.html), which has just been announced and provides various proof strategies to automate such proofs. -- -------------------------------------------------------------------- Holger Pfeifer Tel.: +49 (0)731 / 50-24124 Abt. Künstliche Intelligenz Fax: +49 (0)731 / 50-24119 Universität Ulm pfeifer@ki.informatik.uni-ulm.de D-89069 Ulm http://www.informatik.uni-ulm.de/ki/pfeifer.html --------------------------------------------------------------------

**References**:**Proofing problem***From:*Wilfried Steiner <e9625095@student.tuwien.ac.at>

- Prev by Date:
**Proofing problem** - Next by Date:
**Re: Proofing problem** - Prev by thread:
**Proofing problem** - Next by thread:
**Re: Proofing problem** - Index(es):