-decidability over the reals

DOI10.1109/LICS.2012.41zbMATH Open1364.03065OpenAlexW2128612513MaRDI QIDQ2986807FDOQ2986807

Authors Sicun Gao, Jeremy Avigad, Edmund Clarke

Publication date 16 May 2017

Published in 2012 27th Annual IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

computable analysisdecision proceduresfirst-order theories over the reals

Mathematics Subject Classification ID

Computation over the reals, computable analysis (03D78) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15)

Abstract: Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any L_F-sentence varphi containing only bounded quantifiers, and any positive rational number delta, decides either "varphi is true", or "a delta-strengthening of varphi is false". Under mild assumptions, for a C-computable signature F, the delta-decision problem for bounded Sigma_k-sentences in L_F resides in (Sigma_k^P)^C. The results stand in sharp contrast to the well-known undecidability results, and serve as a theoretical basis for the use of numerical methods in decision procedures for nonlinear first-order theories over the reals.

Recommendations

• \(\delta \)-complete decision procedures for satisfiability over the reals
• Delta-decision procedures for exists-forall problems over the reals
• Decidability in elementary analysis. I
• Quasi-decidability of a fragment of the first-order theory of real numbers
• \(\delta\)-uniform BSS machines

Cited in

(16)

• Monitoring bounded LTL properties using interval analysis
• Quasi-decidability of a fragment of the first-order theory of real numbers
• Towards physical hybrid systems
• On Σ‐definability without equality over the real numbers
• Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability
• scientific article; zbMATH DE number 1390084 (Why is no real title available?)
• \(\delta \)-complete decision procedures for satisfiability over the reals
• Relating syntactic and semantic perturbations of hybrid automata
• Delta-decision procedures for exists-forall problems over the reals
• The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Decidability in analysis
• scientific article; zbMATH DE number 177484 (Why is no real title available?)
• Verified propagation of imprecise probabilities in non-linear ODEs
• The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Decision problems and round-off machines
• Decidability and confluence of \(\beta\eta\text{top}_ \leqslant\) reduction in \({\mathbb{F}}_ \leqslant\)

This page was built for publication: \(\delta\)-decidability over the reals

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2986807)