AF: Small: Quantifier elimination by group analysis

该项目将通过使用群体分析来解决量词消除问题。量词消除是采用复杂公式（带量词）并生成等效但更简单的公式（不带量词）的问题。科学和工程中的许多重要且重要的问题都可以归结为量词消除问题。因此，量词消除方面的任何进展都可能对科学和工程产生重大而广泛的影响。群分析是一种应用群论来简化或阐明难题的方法，如代数和微分伽罗瓦理论、李群和李代数理论等。特别是，群分析显着扩展了科学和工程中出现的各种微分方程的实际可解性。 该项目旨在通过使用群体分析在量词消除方面取得进一步进展。 主要思想是在进行量词消除之前，通过群分析来简化量化公式。初步调查表明，当问题中存在隐藏的群结构时（由于自然界中存在各种内在对称性，这种情况经常发生），群分析可以提供显着的加速。 该项目的科学目标是开发理论、算法和软件包，供科学家和工程师用来解决更多的重要问题。该项目的教育目标是培养未来的研究人员（博士生）并通过 REU 项目和独立研究激励本科生。

This project will tackle quantifier elimination by using group analysis. Quantifier elimination is a problem of taking a complex formula (with quantifiers) and producing an equivalent but simpler formula (without quantifiers). Numerous non-trivial and important problems in science and engineering can be reduced to quantifier elimination problems. Hence any progress in quantifier elimination can have significant and broad impact on science and engineering. Group analysis is an approach of applying group theory to simplify or elucidate a difficult problem, as manifested in algebraic and differential Galois theories, theories of Lie groups and Lie algebras, among many others. In particular, the group analysis significantly extended the practical solvability of various differential equations arising in science and engineering. This project aims to make further progress in quantifier elimination by using group analysis. The main idea is to simplify a quantified formula via group analysis before carrying quantifier elimination. Preliminary investigation shows that group analysis could provide dramatic speed-up, when there is a hidden group structure in the problem (which is often the case due to various intrinsic symmetries in the nature). The scientific goal of the project is to develop theory, algorithms, and software packages that will be used by scientists and engineers for solving ever more non-trivial problems. The educational goal of the project is to train future researchers (PhD students) and to inspire undergraduate students via REU programs and independent studies.