QUICK DOCUMENTATION
--------------------
FIELD and CANCEL-BY are the main strategies provided by this package.
However, it also includes a set of strategies for arithmetic and
logic manipulation of formulas. They are referred as "extrategies".
FIELD is a simplification procedure for the field of real numbers. It
was originally based on Field of Coq V7 (Mayero, Delahaye), but it has
been extensively adapted to cope with PVS idiosyncrasies. First, it
removes inverses, and then it simplifies using PVS decision
procedures. It also tries to prove that inverses are not null.
CANCEL-BY tries to eliminate a factor term of a relational formula.
First, it divides the formula by the factor term, and then it
simplifies the formula by using PVS decision procedures. It also
tries to prove that the common term is not null. CANCEL-FORMULA combines
Manip's FACTOR and CANCEL-BY to cancel common factors in a relational
formula.
- GRIND-REALS: Applies GRIND with real_props.
- REAL-PROPS: Rewrites with real_props in a given formula (or set of formulas).
- REPLACES: Iterates REPLACE using a list of formulas. In contrast to REPLACE, HIDE? T is the default.
- NEG-FORMULA: Negates both sides of a relational formula.
- ADD-FORMULAS: Adds two relational formulas.
- SUB-FORMULAS: Subtracts two relational formulas.
- BOTH-SIDES-F: Applies an arbitrary function both sides of a relational formula.
- NAME-DISTRIB: Introduces new names to block distributive laws in a list of relational formulas.
- SPLASH: Splits, in an asymmetrical way, a conjunction in the consequent (or a disjunction in the antecedent).
- SKEEP: Skolemizes a universal formula by keeping the original names of the quantified variables.
- INSTEEP: Instantiates an existential formula by using the same names of the quantified variables.
- CANCEL-FORMULA: Factorizes common terms in a formula and then cancels them.
- SKODEF: Instantiates quantified formulas appearing in the antecedent and having the form
FORALL (..x..):x=... AND ... IMPLIES ... or in the consequent and having the form EXISTS (..x..):x=... AND ....
- SKODEF*: Iterates SKODEF.
- REDLET: Reduces, in a controlled way, let-in expressions.
- REDLET*: Iterates REDLET.
- SKOLETIN: Skolemizes let-in expressions.
- SKOLETIN*: iterates SKOLETIN.
EXAMPLES
--------
Check the files in the directory nasalib/examples.
FURTHER INFORMATION
-------------------
- Field: http://shemesh.larc.nasa.gov/people/cam/Field
- Extrategies: http://shemesh.larc.nasa.gov/people/cam/Extrategies
- NASA PVS Library: http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library
HELP
----
For a complete list of strategies in Field and Extrategies, try the
proof commands (field-about) and (extrategies-about).
BUGS
----
Submit bugs to Cesar Munoz ([email protected]).
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
