New versions of Manip and Field strategies

[Ben Di Vito <b.l.divito@larc.nasa.gov>]

Announcement: Manip 1.1 and Field.2a
------------------------------------

Updated versions of our prover strategy packages, Manip and Field, are
now available for PVS 3.1.  Both offer enhanced automation for
arithmetic deduction.  Manip carries out user-directed manipulation
steps.  Field works with Manip to achieve higher level simplification.
Both packages exploit new 3.0/3.1 features for loading libraries,
making installation simpler and more robust.

You may retrieve these libraries directly:

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

    Field.2a : http://research.nianet.org/~munoz/Field/

Manip 1.1 includes modest improvements over 1.0.  Factoring now takes
integer coefficients into account.  Error checking of user inputs has
been expanded.

Field.2a is an extensive revision of Field.1h; it is faster, smarter,
and more stable.  To enhance existing capabilities for simplification
(FIELD, CANCEL-BY, etc), Field.2a adds several new strategies:

- REDLET, SKOLETIN, and their iterations REDLET* and SKOLETIN*
  control the way let-in expressions are reduced.

- SKEEP allows you to Skolemize to variables like "x" instead of "x!1".

- CANCEL-FORMULA combines Manip's FACTOR and Field's CANCEL-BY so you
  need not provide a common factor.

- New key options NODISTRIB in GRIND-REALS and DISTRIB? in REAL-PROPS
  control the application of distributive laws.

We welcome comments and user reports.

Best regards,

Ben Di Vito
Cesar Munoz

-----------

Ben L. Di Vito
1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681 USA
b.l.divito@larc.nasa.gov
http://shemesh.larc.nasa.gov/~bld

Cesar A. Munoz 
National Institute of Aerospace
144 Research Drive
Hampton, VA 23666, USA
munoz@nianet.org
http://research.nianet.org/~munoz