Efficient solution of a class of quantified constraints with quantifier prefix exists-forall

DOI10.1007/S11786-014-0195-8zbMath1302.65118arXiv1312.6155OpenAlexW1999758876MaRDI QIDQ475420

Stefan Ratschan, Milan Hladík

Publication date: 27 November 2014

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1312.6155

zbMATH Keywords

constraint solvinginterval computationdecision procedures

Mathematics Subject Classification ID

Interval and finite arithmetic (65G30) Global methods, including homotopy approaches to the numerical solution of nonlinear equations (65H20) Algorithms with automatic result verification (65G20)

Uses Software

• QEPCAD
• Sostools
• REDLOG
• RSOLVER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Weak and strong solvability of interval linear systems of equations and inequalities
• Efficient handling of universally quantified inequalities
• Termination of rewriting
• Testing positiveness of polynomials
• Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
• Search heuristics for box decomposition methods
• Guaranteed tuning, with application to robust control and motion planning
• Revised CPA method to compute Lyapunov functions for nonlinear systems
• Constructing invariants for hybrid systems
• Providing a Basin of Attraction to a Target Region of Polynomial Systems by Computation of Lyapunov-Like Functions
• Interval Methods for Systems of Equations
• Linear interval inequalities
• Subdivision Direction Selection in Interval Methods for Global Optimization
• Automatic Generation of Polynomial Loop Invariants
• SOSTOOLS and Its Control Applications
• Verification and synthesis using real quantifier elimination
• Efficient solving of quantified inequality constraints over the real numbers
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• A posteriori direction selection rules for interval optimization methods

This page was built for publication: Efficient solution of a class of quantified constraints with quantifier prefix exists-forall