Pseudo-Complex Quantifier Elimination
For researchers in symbolic computation and logic, this provides a practical approach to complex quantifier elimination, but the work is incremental as it relies on existing real quantifier elimination methods.
The paper presents a framework for quantifier elimination over complex numbers by reducing to real quantifier elimination and reinterpreting results in a complex setting, with a prototypical implementation in Logic1. No concrete performance numbers are provided.
We describe the design of a quantifier elimination framework for the complex numbers in the language of ordered rings supplemented with symbols for the imaginary unit, real parts, imaginary parts, and conjugates. Technically, we use a reduction to real quantifier elimination followed by a heuristic reinterpretation of the results within our complex framework. We present computational examples using a prototypical implementation of our approach in our Python-based open-source system Logic1.