Enhanced CAD-Based Quantifier Elimination With Multiple Equational Constraints
For researchers using CAD-based quantifier elimination, this work offers incremental enhancements that improve output detail and computational efficiency in specific scenarios.
This paper improves cylindrical algebraic decomposition (CAD) based quantifier elimination for formulas with multiple equational constraints, providing more detailed output by partitioning parameter space and achieving efficiency gains by reducing the second CAD equational projection step under certain conditions.
This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present in the given input formula $ϕ^*$. The first enhancement provides more detail in the output when there is a conceptual partition of the set of variables of $ϕ^*$ into parameters and unknowns. In such cases, we describe how to partition the parameter space so that: (1) in each open set of the partition the number $ν$ of associated unknowns is a finite constant or is infinite; and (2) for each such open set for which $ν$ is finite, an expression for the unknowns in terms of the parameters is provided. The second enhancement is an efficiency gain achievable in certain situations. Indeed, when certain conditions are met, the second CAD equational projection step can be reduced more significantly than is supported by the prior existing theory. Relevant theorems and worked examples for both enhancements are provided. Application areas include approximation theory, cuspidal manipulator classification, and biological/chemical systems.