Quasi-decidability of a fragment of the first-order theory of real numbers
From MaRDI portal
Publication:2013319
DOI10.1007/s10817-015-9351-3zbMath1437.03047arXiv1309.6280OpenAlexW1835316325WikidataQ114226109 ScholiaQ114226109MaRDI QIDQ2013319
Stefan Ratschan, Peter Franek, Piotr Zgliczyński
Publication date: 17 August 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1309.6280
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Computation over the reals, computable analysis (03D78)
Related Items (5)
Solving equations and optimization problems with uncertainty ⋮ On computability and triviality of well groups ⋮ Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test ⋮ Relating syntactic and semantic perturbations of hybrid automata ⋮ Effective topological degree computation based on interval arithmetic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Complexity of computing topological degree of Lipschitz functions in n dimensions
- A history of algebraic and differential topology 1900--1960
- Discrete semantics for hybrid automata. Avoiding misleading assumptions in systems biology
- MetiTarski: An automatic theorem prover for real-valued special functions
- An efficient degree-computation method for a generalized method of bisection
- A note on epsilon-inflation
- Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993
- Quantified constraints under perturbation
- On existence and uniqueness verification for non-smooth functions
- On the existence theorems of Kantorovich, Miranda and Borsuk
- δ-Complete Decision Procedures for Satisfiability over the Reals
- Delta-Decidability over the Reals
- Satisfiability of Systems of Equations of Real Analytic Functions Is Quasi-decidable
- Robust Satisfiability of Systems of Equations
- GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
- Safety Verification of Non-linear Hybrid Systems Is Quasi-Semidecidable
- Smoothed analysis of algorithms
- Introduction to Interval Analysis
- Die Nichtkonstruktivität des Brouwerschen Fixpunktsatzes
- Interval Methods for Systems of Equations
- Differential Topology
- Computing the Brouwer Degree in R 2
- Computation of Topological Degree Using Interval Arithmetic, and Applications
- The Undecidability of the Existence of Zeros of Real Elementary Functions
- Computability and Representations of the Zero Set
- Effective topological degree computation based on interval arithmetic
- Convergent approximate solving of first-order constraints by approximate quantifiers
- Efficient solving of quantified inequality constraints over the real numbers
- Existence Tests for Solutions of Nonlinear Equations Using Borsuk's Theorem
This page was built for publication: Quasi-decidability of a fragment of the first-order theory of real numbers
