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.
翻译:本文提出了两项针对柱形代数分解(CAD)的量词消去(QE)方法的改进,适用于输入公式$φ^*$中包含多个等式约束的情形。第一项改进在将$φ^*$的变量集概念性地划分为参数与未知量时,为输出结果提供更细致的信息。在此类情况下,我们描述了如何划分参数空间,使得:(1)在划分的每个开集中,关联未知量的个数$ν$为有限常数或无穷大;(2)对于每个$ν$有限的此类开集,给出未知量关于参数的表达式。第二项改进是特定条件下可实现效率提升。实际上,当满足某些条件时,第二重CAD等式投影步骤的缩减程度可超过现有理论的支持范围。本文提供了两项改进的相关定理与示例验证。应用领域包括逼近理论、尖点机械臂分类以及生物/化学系统。