[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Proof assistant needed for non-linear arithmetic
> 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