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

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

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.