PVS 2.3 Experimental Features - the inst! command

syntax: (inst! (&optional (fnums *) subst (where *) copy? (if-match best) complete? (relativize? T)))

effect: Like INST? this strategy extends the capabilities of the INST rule, but it tries to be more careful than INST? in selecting candidate instantiations. INST! simultaneously searches for instantiations for the top-level, existential strength variables of all of the FNUMS formulas. Hereby, it restricts its search to the formulas in WHERE. First, a full case split for the formulas specified by FNUMS and WHERE is computed; e.g. a formula in the hypothesis of the form (EXISTS (x: { y: T | P(y)}): Q(x) => R(x)) gives rise to three sequents in the split corresponding the the two parts of the implication and the predicate subtype. If the RELATIVIZE? flag is unset, however, then predicate subtypes are being ignored in the split. In the next step, a sequence of instantiations is generated by unifying complementary pairs in the sequents of the case splits.

If such an instantiation can not be found then the current proof sequent is left unchanged. If there are several possible complete set of instantiations then INST! chooses a heuristically best one if the IF-MATCH flag is set to BEST. This is done by giving a score to each candidate instantiation, which measures the prospect of continuing the proof construction. The score roughly corresponds to the number of sequents in the full case split of the current proof sequent for which one can find complementary atoms after applying the instantiation.

If IF-MATCH is ALL, then the command returns all found instantiations of the FNUMS. For the other alternatives of the IF-MATCH flag see the description of INST?.

The COPY? argument works exactly as in QUANT and is used to retain a copy of the quantified formula. Note that an uncopied, quantified formula is automatically hidden.

The COMPLETE? argument specifies whether or not incomplete instantiations are being considered.

usage: see (inst?)

errors: "Could not find an existential-strength formula."
"No suitable instantiation found"

notes: This strategy is included for experimental purposes only and its functionality (and speed!) is most likely to change in future releases. Thus, proof scripts that are using it are likely to break in the future!

Last modified: Tue Jun 22 15:10:33 PDT 1999

[ PVS Home Page]