-decidability over the reals

DOI10.1109/LICS.2012.41zbMATH Open1364.03065arXiv1204.6671OpenAlexW2128612513MaRDI 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)

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.

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

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

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)

Cited In (16)

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

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)