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

*To*: R.W.Butler@larc.nasa.gov*Subject*: Re: Proof assistant needed for non-linear arithmetic*From*: Harald Ruess <ruess@csl.sri.com>*Date*: Fri, 14 Aug 1998 16:43:35 +0200*Cc*: pvs@csl.sri.com*Cc*: ruess@csl.sri.com*In-reply-to*: <199808101233.IAA01000@air58.larc.nasa.gov>(rwb@air58.larc.nasa.gov)*Reply-to*: ruess@csl.sri.com

> Now wouldn't it be nice if there were a proof assistant running on top of > PVS that you could use as follows: > > {-1} n!1 < m!1 > |------- > {1} n!1 / m!1 < 1 > > Rule? (DIVIDE_BOTH_SIDES_BY "m!1" -1) > The proof assistant would then look through the prelude, find the > appropriate LEMMA and instantiate it for you. The (defined) pvs strategy `both-sides' provides exactly this feature. In your example, calling the strategy (both-sides "*" "m!1") (or, equivalently, (both-sides "/" "m!1" -1)) on the goal above yields a goal (subgoals) in a form that can be handled by the decision procedures. > It seems to me that this could be developed by graduate students as a > class project or a Master's thesis.? Admittedly, the strategy both-sides is rather slow and it is not the most reliable one either. So there is some need for improvement... Developing a PVS strategy that incorporates the mathematical skills of a 7th, 8th,... grader for dealing with non-linear equations (including transcendental functions) in a systematic way would not only be an interesting thesis but also be useful for many applications. Has anybody written such a thing for PVS? Best regards, Harald Ruess

**References**:**Proof assistant needed for non-linear arithmetic***From:*"Ricky W. Butler" <rwb@air58.larc.nasa.gov>

- Prev by Date:
**Proof assistant needed for non-linear arithmetic** - Next by Date:
**Re: SPAM on pvs email list** - Prev by thread:
**Proof assistant needed for non-linear arithmetic** - Next by thread:
**Re: SPAM on pvs email list** - Index(es):