Efficient Solving of Quantified Inequality Constraints over the Real Numbers

2002/11/14 by Stefan Ratschan, Ratschan, Stefan · 1 citation
Computer Science · #Constraint Satisfaction and Optimization #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #G.1.0 #I.2.3 #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Numerical Analysis (math.NA)

paper · pdf · doi:10.48550/arxiv.cs/0211016

openalex publication_date 2002/11/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Let a quantified inequality constraint over the reals be a formula in the first-order predicate language over the structure of the real numbers, where the allowed predicate symbols are ≤ and <. Solving such constraints is an undecidable problem when allowing function symbols such sin or cos. In the paper we give an algorithm that terminates with a solution for all, except for very special, pathological inputs. We ensure the practical efficiency of this algorithm by employing constraint programming techniques.

Cited by

• Approximate Axiomatization for Differentially-Defined Functions

Related

• Applications of Quantified Constraint Solving over the Reals -- Bibliography
• Convergent Approximate Solving of First-Order Constraints by Approximate Quantifiers
• An Efficient Algorithm for a Sharp Approximation of Universally Quantified Inequalities
• Solving Composed First-Order Constraints from Discrete-Time Robust Control
• The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable