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

Manipulation strategies available



PVS prover users,

After making various fixes and improvements, I am releasing version
1.0 of a PVS strategy package called Manip, which was first announced
on 1 November 2001.  Although the original goal was to automate
certain sequent manipulations to simplify proofs involving nonlinear
arithmetic, there are now features included that benefit interactive
proving in general.  An extended expression notation, for example,
enables users to identify and operate on subexpressions without
clipping fragments from the current sequent.

To retrieve the package, visit this page:

  http://shemesh.larc.nasa.gov/people/bld/manip.html

The strategies work with PVS version 2.3 or 2.4.  User documentation
is included in the tar file.

I expect to develop Manip further and issue future releases, probably
without announcement.  I welcome suggestions for documentation
improvements, requests for new or altered features, and feedback on
user experiences.  I also encourage bug reports, of course.


Best regards,

Ben Di Vito


-----------

Ben Di Vito                     b.l.divito@larc.nasa.gov
1 South Wright Street, MS 130   http://shemesh.larc.nasa.gov/~bld
NASA Langley Research Center    voice: +1-757-864-4883
Hampton, VA 23681   USA         fax:   +1-757-864-4234