[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