PVS 2.3 Experimental Features - the (qe) strategy

syntax: (qe &optional (fnums *) verbose?)

effect: Replaces the formulas specified by FNUMS one-by-one with an equivalent, quantifier-free formula if such a form can be constructed; otherwise the formula is left unchanged.

Currently, only elimination of quantifiers over the Booleans, the integers, the rationals, the reals, and predicate subtypes thereof are supported. Moreover, the procedure usually only works for linear arithmetic.

QE works by eliminating quantifiers inside-out and replacing universal quantifiers with the dual existential form. For a quantifier-free body, the disjunctive normal form is computed and elimination is performed separately for each disjunct. If the current binding is of finite type, the procedure simple forms the disjunction of the bodies replaced with all possible values for this type. Otherwise, the procedure tries to find a concrete value for the existentially quantified value by using the PVS decision procedures. If such a value exists, then the quantifier is being eliminated by substituting this value into the body of the current subformula. If such a solved form can not be found, the procedure applies Fourier-Motzkin elimination on inequalities.

Quantifier elimination may fail if a bound variable occurs in the scope of an uninterpreted function. However, the procedure does eliminate bound occurrences of integer variables from the scope of the FLOOR function. The FLOOR function is also used to guarantee the existence of an integer solution of the current constraint by adding conjuncts like e = FLOOR(e) to the eliminated form.

The VERBOSE? flag set to T causes the display of trace output. The exact reading of this trace is subject to change, and thus not being described here.

errors: "Unable to eliminate EXISTS (...): ..."
At least one of the quantifiers could not be eliminated. In this case, the current formula is left unchanged.

"Term ... may contain nonlinearity"
Solving ... did not succeed, supposedly because of some nonlinearity.

notes: The capabilities of this strategy are currently being extended to handle quantifiers involving finite types (besides Booleans), arrays, and datatypes like lists.

Last modified: Thu May 6 14:33:45 PDT 1999

[ PVS Home Page]