[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
New versions of Manip and Field strategies
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
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.
Ben Di Vito
Ben L. Di Vito
1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681 USA
Cesar A. Munoz
National Institute of Aerospace
144 Research Drive
Hampton, VA 23666, USA