Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: field-guide.txt Sprache: Text

Original von: PVS^©

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.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.