NASA PVS Library V5.2: What's New?

• library "fs" added. It is just a holding place for theories that should be in finite_sets. These will be moved to finite_sets directory in the next release of PVS.
• reals library Moved abs_props and real_facts into reals library. NOTE (stop-rewrite "abs_0") (stop-rewrite "abs_nat") may be helpful in repairing broken proofs that use analysis library or reals@abs_lems. Can also use AUTO_REWRITE- in theory.
• vectors library Added vectors_sign theories to vectors library. Added cross_3D and sigma over vector-valued functions.
• reals library The product operator added. A generic theory is provided in product.pvs, which is similar to sigma.pvs. The following theories provide additional theorems for specific domains: product_below, product_int, product_nat, product_posnat, product_upto.
• structures library An experimental alternate finite sequences theory "fseqs" added.
• Number Theory library contents moved to "numbers" directory.
• New scott and sigma_set libraries provided by David Lester of Manchester University.
• series library New lemmas added to series library about absolute convergence.
• algebra library Factor groups defined.
• New Manip, New Interval, New versions installed.
• trig_fnd library improvements to atan_approx and trig_approx
• reals library: Improved sigma definition (simpler IF-THEN-ELSE). NOTE: this will break some proofs, but an extra (expand "sigma") or replacing (expand"sigma") with (rewrite "sigma_rew") will often easily fix the proofs. The older versions are retained as old_sigma-*.pvs. Added reals@quad_minmax which supercedes quadratic_minmax.
• vectors library Theories (closest_approach*) improved
• new topology library: Thanks to David Lester!
• graphs library: Menger's Theorem now general due to Jon Sjogren, AFOSR
• complex library: updated by David Lester
• new co_structures library: thanks Jerry James!
• reals library: sigma generalized to allow index ranges to fall outside of domain of T when high < low.
• series library: definition of powerseq was simplified.
• intervals library: New library created by Cesar Munoz. See http://research.nianet.org/~munoz/Interval/ for more details.
• graphs library: Jon Sjogren (AFOSR) has add two new theories: mappings and matroids
• sets_aux library: split into sets_aux and orders libraries.
• float library: Sylvie Boldo (ENS-Lyon) has developed a new floating-point arithmetic library. Thanks Sylvie!
• UNDER-DEVELOPMENT libraries can be downloaded from the UNDER_DEVELOPMENT tar file.
• lnexp and lnexp_fnd libraries: lnexp now contains an axiomatic version. The foundational version is in lnexp_fnd.
• trig library: Updated to match foundational version (trig_fnd).
• sets_aux library: Jerry James (University of Kansas) and Alfons Geser (NIA) have worked to generalize our library. The library provides more efficient results for bounded sets, lattices and complete latices. It supports reasoning about least upper bounds and greatest lower bounds in a more general framework.
• ln_exp library: The approximation for "ln" has been updated. Infinite series for ln(1+x), |x| < 1 added.
• complex library: David Lester of Manchester University has developed a theory for complex numbers.
• algebra library: David Lester of Manchester University has developed a new algebra library that replaced the previous algebra library.
• structures library: Lee Pike has made significant extensions to our "bags" theories.
• analysis library: Revised the definition of the Riemann Integral. All of the axioms have now been proved. Have changed the names of over 70 lemmas. See file "name-change-help.txt". Change of variable theorem for integrals added. See integral_chg_var. Also integral_dif_doms added.
• trig_fnd library: David Lester of Manchester University has proved all of the AXIOMS of our trig library. Thanks, David!! These foundational proofs are available in "trig_fnd". We are working on using the PVS 3.2 theory interpretations to meet two important goals: (1) blueuce the amount of stuff that needs to be typechecked when you want to use trig functions, and (2) insure that all of the AXIOMS are sound.
• series library: David Lester has generalized Taylor's Theorem and others. All of the axioms are now proved. Convergence of Taylor series. Theorem "integral_powerseries" completed.
• General Purpose Strategy Packages: Manip and Field strategies updated to PVS 3.2. All strategy packages and PVSio available in the tar file.