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.
