AF: Small: Comprehensive Groebner, Parametric GCD Computations and Real Geometric Reasoning

物理现象和网络物理系统的数学建模及其行为预测是科学研究的标志。检查建模过程的有效性是这种分析方法的关键组成部分。多项式通常是最简单的工具之一。为了模拟成分大小和外生变化的变化，多项式中的变量通常分为参数和非参数。一个素数和简单的例子是二次方程A * square(x) + b * x + c，它的参数A、b和c的取值不同，它的行为也有很大的不同，在某些参数值下有等解，在其他值下有实解，在不同参数值下有复解或无解。模型的结构特性是用参数来表示的，因为对于不同的参数，模型的行为会有很大的不同。开发能够识别模型表现明显不同的不同类型参数值的算法变得至关重要。这样的分析将有利于许多不同的应用，包括机器人，运动学，建模，计算机视觉，基于分子建模和化学关系的药物设计，遗传途径，以及集成控制，硬件和软件的众多网络物理系统。该项目具有所有的理论、实现和应用组件。本项目研究的问题的基本性质及其在许多领域的应用可能会吸引具有不同背景的广泛学生，特别是来自代表性不足的群体的研究生和本科生。该项目生成的材料将被整合到新墨西哥大学（UNM）研究人员正在教授的自动推理、数学建模和网络物理系统课程中。通过参与这些调查，新墨西哥州的国家实验室和整个社会所面临的挑战和诸多好处将吸引人们的参与，并为新墨西哥大学的学生提供不同的职业机会。本项目由计算算法基金会和通信基金会以及促进竞争研究的既定计划（EPSCoR）共同资助。该项目将涉及求解参数多元多项式系统的符号和实几何推理的算法开发研究。所使用的主要工具是综合格罗布纳基计算及其在其他符号计算算法中使用的许多基本原语，包括多项式的参数最大公除法。这些算法将作为开发一种实用的、不完整的、近似量词消除方法的基础，用于复数和实数，目的是为应用程序产生有意义和有用的输出。与Tarski的方法和基于Collins柱面代数分解（CAD）的相关算法不同，多项式等式将使用全面的Groebner基计算。我们将探讨平方和方法和基于二次形式的实根计数的不等式的Positivstellensatz结果。格罗布纳基计算技术将适用于多项式不等式，以发展启发式方法来确定多项式的非负性。由于这些问题具有非常高的计算复杂性，它们在实际应用中的相关性要求开发针对应用问题的特殊启发式方法。研究小组在定理证明及其应用方面的经验将被利用来开发一个软件工具。将探索启发式方法以使这些实现更有效。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Mathematical modeling of physical phenomena and cyber-physical systems and prediction from their behavior are hallmarks of scientific investigation. Checking validity of the modeling process is a critical component of this analytical approach. Polynomials are often one of the simplest tools employed in this endeavor. In order to model variations in the size of components and exogenous changes, variables in polynomials are typically classified into parameters and non-parameters. A prime and simple example is that of a quadratic equation a* square(x) + b * x + c, which behaves very differently for different values of its parameters a, b and c. It has equal solutions under certain parameter values, real solutions under other values and complex solutions or no solution at all under different parameter values. Structural properties of models are expressed using parameters since for different parameters, model can behave significantly different. It becomes critical to develop algorithms that can identify different classes of parameter values for which a model behaves significantly different. Such analysis will benefit many diverse applications including robotics, kinematics, modeling, computer vision, drug design based on molecular modeling and chemical relations, genetic pathways, and numerous cyber physical systems integrating control, hardware and software. The project has all of the theoretical, implementation and application components. The fundamental nature of problems investigated in this project and their application in many domain are likely to appeal to a broad set of students with diverse backgrounds especially from under-represented groups, both graduate and undergraduate. The material generated from this project will be integrated into courses on automated reasoning, mathematical modeling and cyber-physical systems that the researchers at the University of New Mexico (UNM) are teaching. The challenges offered and numerous benefits seen for the national laboratories in New Mexico and society at large by engaging in these investigations will attract participation and offer different career opportunities to the UNM students. This project is jointly funded by Algorithmic Foundations in Computing and Communications Foundations and the Established Program to Stimulate Competitive Research (EPSCoR).The project will involve algorithmic development research in solving parametric multivariate polynomial systems symbolically and real geometry reasoning. The main tool used is that of comprehensive Groebner basis computations and their use in many basic primitive used in other symbolic computation algorithms including parametric greatest common division of polynomials. These algorithms will serve as a basis for the development of a pragmatic, incomplete, approximate quantifier elimination approach over the complex numbers and the reals with the goal of producing meaningful and useful output for applications. Unlike Tarski's method and related algorithms based on Collins' Cylindrical Algebraic Decomposition (CAD), comprehensive Groebner basis computations will be used for polynomial equalities. Results about Positivstellensatz for inequalities using the sum of squares approach and real root counting based on quadratic forms will be explored. Techniques for Groebner basis computations will be adapted for polynomial inequalities to develop heuristics to decide non-negativity of polynomials. Since these problems are of very high computational complexity, their relevance in practical applications calls for developing special heuristics specific to application problems. The research team's experience in theorem proving and its application will be exploited to develop a software tool. Heuristics will be explored to make these implementations efficient.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.