Accession Number:

ADA608079

Title:

On Quantifer Elimination by Virtual Term Substitution

Descriptive Note:

Technical rept.

Corporate Author:

NAVAL ACADEMY ANNAPOLIS MD DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

2005-08-24

Pagination or Media Count:

0.0

Abstract:

This paper presents a new look at Weispfennings method of quantifier elimination by virtual term substitution and provides two important improvements. Virtual term substitution eliminates a quantified variable by substituting formulas in the remaining variables for each atomic formula in which the quantified variable appears. This paper investigates the polynomials that arise in substitution formulas Weispfenning proposed and, based on this examination, provides a simpler substitution for the general case, and alternate substitutions for several commonly occurring situations. Providing alternate substitutions allows virtual term substitution to make choices that produce simpler output.

Subject Categories:

  • Numerical Mathematics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE