Pseudo-Complex Quantifier Elimination

2026/04/29 by Nicolas Faroß, Thomas Sturm · 1 voice
Computer Science · #Algebra over a field #Formal Methods in Verification #Heuristic #Heuristics #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Quantifier (linguistics) #Quantifier elimination #Reduction (mathematics) #cs.LO #cs.SC

paper · pdf · doi:10.48550/arxiv.2604.26400

openalex publication_date 2026/04/29 · arxiv published 2026/04/29 · openalex created_date 2026/05/01 · arxiv updated 2026/06/11 · openalex updated_date 2026/07/28

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.

Citations

• Parametric Toricity of Steady State Varieties of Reaction Networks
• A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
• Data Structures for Weighted Matching and Extensions to b-matching and\n f-factors
• Algorithms for Computing Triangular Decompositions of Polynomial Systems
• Real quantifier elimination is doubly exponential

Discussions

• Nicolas Faro{\ss}, Thomas Sturm: Pseudo-Complex Quantifier Elimination https://arxiv.org/abs/2604.26400 https://arxiv.org/pdf/2604.26400 https://arxiv.org/html/2604.26400 [bsky, 0 points, 0 comments]

Related

• Elementary recursive quantifier elimination based on Thom encoding and sign determination
• A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Iterated Resultants and Rational Functions in Real Quantifier Elimination
• Applying Linear Quantifier Elimination