Pseudo-Complex Quantifier Elimination

TL;DR

This paper introduces a quantifier elimination framework for complex numbers using a reduction to real quantifier elimination, implemented in an open-source Python system, enabling computational analysis within complex algebraic structures.

Contribution

It presents a novel approach combining real quantifier elimination with heuristic reinterpretation for complex numbers, implemented in an open-source Python system.

Findings

Successful computational examples demonstrating the framework's effectiveness.

Implementation in an open-source Python system facilitates practical use.

Framework bridges real and complex quantifier elimination techniques.

Abstract

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.