Quasi-decidability of a fragment of the first-order theory of real numbers
From MaRDI portal
(Redirected from Publication:2013319)
Abstract: In this paper we consider a fragment of the first-order theory of the real numbers that includes systems of equations of continuous functions in bounded domains, and for which all functions are computable in the sense that it is possible to compute arbitrarily close piece-wise interval approximations. Even though this fragment is undecidable, we prove that there is a (possibly non-terminating) algorithm for checking satisfiability such that (1) whenever it terminates, it computes a correct answer, and (2) it always terminates when the input is robust. A formula is robust, if its satisfiability does not change under small perturbations. As a basic tool for our algorithm we use the notion of degree from the field of (differential) topology.
Recommendations
- scientific article; zbMATH DE number 4150340
- Decidability in the Constructive Theory of Reals as an Ordered ℚ‐vectorspace
- First-order decidability and definability of integers in infinite algebraic extensions of the rational numbers
- scientific article; zbMATH DE number 7340151
- Complexity of deciding the first-order theory of real closed fields
- scientific article; zbMATH DE number 16631
- \(\delta\)-decidability over the reals
- Automated Deduction – CADE-20
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Decidability of Definability Issues in the Theory of Real Addition
Cites work
- scientific article; zbMATH DE number 52121 (Why is no real title available?)
- scientific article; zbMATH DE number 977420 (Why is no real title available?)
- scientific article; zbMATH DE number 1094954 (Why is no real title available?)
- scientific article; zbMATH DE number 1950480 (Why is no real title available?)
- scientific article; zbMATH DE number 2090047 (Why is no real title available?)
- scientific article; zbMATH DE number 794708 (Why is no real title available?)
- scientific article; zbMATH DE number 1424031 (Why is no real title available?)
- scientific article; zbMATH DE number 2242595 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- A history of algebraic and differential topology 1900--1960
- A note on epsilon-inflation
- A tutorial on computable analysis
- An efficient degree-computation method for a generalized method of bisection
- Complexity of computing topological degree of Lipschitz functions in n dimensions
- Computability and representations of the zero set
- Computation of Topological Degree Using Interval Arithmetic, and Applications
- Computing the Brouwer Degree in R 2
- Convergent approximate solving of first-order constraints by approximate quantifiers
- Die Nichtkonstruktivität des Brouwerschen Fixpunktsatzes
- Differential Topology
- Discrete semantics for hybrid automata. Avoiding misleading assumptions in systems biology
- Effective topological degree computation based on interval arithmetic
- Efficient solving of quantified inequality constraints over the real numbers
- Existence Tests for Solutions of Nonlinear Equations Using Borsuk's Theorem
- GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
- Interval Methods for Systems of Equations
- Introduction to Interval Analysis
- Mapping degree theory
- MetiTarski: An automatic theorem prover for real-valued special functions
- On existence and uniqueness verification for non-smooth functions
- On the existence theorems of Kantorovich, Miranda and Borsuk
- Quantified constraints under perturbation
- Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
- Robust optimization
- Robust satisfiability of systems of equations
- Safety verification of non-linear hybrid systems is quasi-semidecidable
- Satisfiability of systems of equations of real analytic functions is quasi-decidable
- Smoothed analysis of algorithms
- The Undecidability of the Existence of Zeros of Real Elementary Functions
- Topological degree theory and applications.
- \(\delta \)-complete decision procedures for satisfiability over the reals
- \(\delta\)-decidability over the reals
Cited in
(15)- Relating syntactic and semantic perturbations of hybrid automata
- Solving equations and optimization problems with uncertainty
- Satisfiability of systems of equations of real analytic functions is quasi-decidable
- Robust satisfiability of systems of equations
- Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
- On the computational complexity and geometry of the first-order theory of the reals. I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals
- On computability and triviality of well groups
- First-order decidability and definability of integers in infinite algebraic extensions of the rational numbers
- scientific article; zbMATH DE number 7340151 (Why is no real title available?)
- A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions
- The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable
- \(\delta\)-decidability over the reals
- Robust satisfiability of systems of equations
- On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination
- Effective topological degree computation based on interval arithmetic
This page was built for publication: Quasi-decidability of a fragment of the first-order theory of real numbers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2013319)
