Better Answers to Real Questions

TL;DR

This paper improves extended quantifier elimination over the reals by introducing a post-processing step that converts answers into standard real numbers, enhancing interpretability and practical usefulness.

Contribution

It presents a novel post-processing method that transforms answers from extended quantifier elimination into standard real numbers, making results more accessible.

Findings

Enhanced interpretability of solutions with standard real numbers

Significant improvement in result quality demonstrated on literature examples

Successful application in science and engineering problems

Abstract

We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.