Quasi-decidability of a fragment of the first-order theory of real numbers
From MaRDI portal
Publication:2013319
DOI10.1007/S10817-015-9351-3zbMATH Open1437.03047arXiv1309.6280OpenAlexW1835316325WikidataQ114226109 ScholiaQ114226109MaRDI QIDQ2013319FDOQ2013319
Authors: Peter Franek, Stefan Ratschan, Piotr Zgliczyński 
Publication date: 17 August 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1309.6280
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
Computation over the reals, computable analysis (03D78) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Cites Work
- Robust optimization
- Introduction to Interval Analysis
- Differential Topology
- Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
- On the existence theorems of Kantorovich, Miranda and Borsuk
- Interval Methods for Systems of Equations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A tutorial on computable analysis
- Title not available (Why is that?)
- A note on epsilon-inflation
- Title not available (Why is that?)
- \(\delta \)-complete decision procedures for satisfiability over the reals
- MetiTarski: An automatic theorem prover for real-valued special functions
- Smoothed analysis of algorithms
- On existence and uniqueness verification for non-smooth functions
- Mapping degree theory
- Computability and representations of the zero set
- Existence Tests for Solutions of Nonlinear Equations Using Borsuk's Theorem
- Title not available (Why is that?)
- Title not available (Why is that?)
- Topological degree theory and applications.
- Safety verification of non-linear hybrid systems is quasi-semidecidable
- Efficient solving of quantified inequality constraints over the real numbers
- Title not available (Why is that?)
- Title not available (Why is that?)
- An efficient degree-computation method for a generalized method of bisection
- Complexity of computing topological degree of Lipschitz functions in n dimensions
- Computation of Topological Degree Using Interval Arithmetic, and Applications
- Quantified constraints under perturbation
- A history of algebraic and differential topology 1900--1960
- Discrete semantics for hybrid automata. Avoiding misleading assumptions in systems biology
- Computing the Brouwer Degree in R 2
- The Undecidability of the Existence of Zeros of Real Elementary Functions
- \(\delta\)-decidability over the reals
- Satisfiability of systems of equations of real analytic functions is quasi-decidable
- Effective topological degree computation based on interval arithmetic
- GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
- Robust satisfiability of systems of equations
- Die Nichtkonstruktivität des Brouwerschen Fixpunktsatzes
- Convergent approximate solving of first-order constraints by approximate quantifiers
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
- Title not available (Why is that?)
- A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions
- \(\delta\)-decidability over the reals
- The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable
- 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
Uses Software
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)
