pith. sign in

arxiv: 2605.24263 · v1 · pith:7CPKKRCXnew · submitted 2026-05-22 · 💻 cs.PL · cs.LO

Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability

S. Akshay , Supratik Chakraborty , R. Govind , Aniruddha R. Joshi This is my paper

Pith reviewed 2026-06-30 13:54 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords program synthesisnonlinear real arithmeticSyGuSrealizabilityrational arithmeticsatisfiabilityloop-free programsNRA specifications
0
0 comments X

The pith

Synthesis from nonlinear real arithmetic specifications can produce programs that either output a solution or report none exists, even for unrealizable cases.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops methods to synthesize programs from nonlinear real arithmetic specifications that operate on rational inputs and outputs. Unlike prior syntax-guided synthesis techniques limited to realizable specifications where solutions always exist, the new programs must either produce a valid output or explicitly report that none exists for a given input. The authors prove the general problem is as hard as an open question in number theory and impossible for loop-free programs in the general case. They give a sound and complete algorithm specifically for specifications with a single output variable, show that SyGuS programs work for realizable cases over rationals, and supply a sound but incomplete method for multiple outputs. A prototype tool solves benchmarks unreachable by existing SyGuS implementations.

Core claim

The central claim is that synthesis from arbitrary NRA specifications over rationals is possible in the single-output case via a sound and complete algorithm that produces programs reporting non-existence when appropriate, while for realizable specifications a SyGuS-generated program over reals directly solves the rational version; the general multi-output case admits only a sound algorithm, as the problem is undecidable for loop-free programs and equivalent in hardness to a long-standing open problem in number theory.

What carries the argument

The sound and complete synthesis algorithm for single-output NRA specifications, which uses decision procedures for nonlinear real arithmetic satisfiability over the rationals to decide output existence and construct the program.

If this is right

  • For realizable NRA specifications, existing SyGuS tools can be reused to obtain solutions that work correctly over rationals.
  • The single-output algorithm provides both existence and non-existence reports, enabling synthesis from specifications that are not always realizable.
  • The general algorithm remains sound for multiple outputs, guaranteeing that any program it produces is correct even if it misses some solvable cases.
  • Many previously unreachable benchmarks become solvable by the new approach even when specifications are made realizable.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The hardness reduction to an open number theory problem suggests that further progress on NRA synthesis may depend on advances in deciding rational points on varieties.
  • The single-output completeness result could be tested for scalability by generating families of specifications with increasing degree or number of variables.
  • The rational restriction avoids floating-point issues and may allow direct transfer of the technique to other decidable fragments of real arithmetic.

Load-bearing premise

Effective decision procedures exist for satisfiability of nonlinear real arithmetic formulas over the rationals.

What would settle it

A concrete single-output NRA specification over rationals on which the synthesis algorithm either fails to terminate with a correct program when one exists or outputs a program that produces an invalid result or fails to report non-existence on some input.

Figures

Figures reproduced from arXiv: 2605.24263 by Aniruddha R. Joshi, R. Govind, S. Akshay, Supratik Chakraborty.

Figure 1
Figure 1. Figure 1: Grammar for programs It is not hard to see that programs derived from this grammar are Turing powerful (e.g. counter￾machines can be encoded). Let Prog be a program in the language of the gram￾mar G, and let X be a tuple of variables used in Prog. We use the nota￾tion Prog(X) to denote the fact that Prog does not assign to any variable in X, and instead uses values of these variables as inputs. For A ∈ Q|X… view at source ↗
Figure 2
Figure 2. Figure 2: Run-time scatter-plots of NQSynth with QEPCAD+CVC5, and ModEnum input variable δ, and replaced all (sub-)formulas of the form term1 = term2 by (δ ≥ 0) ∧ (−δ ≤ term1 − term2 ≤ δ). Our second set of benchmarks, called “Geometric”, consists of 51 Non-Linear Real Arithmetic (NRA) specifications motivated by problems in 2- and 3-dimensional geometry. These benchmarks model spatial relationships and bounding pro… view at source ↗
Figure 3
Figure 3. Figure 3: A simple specification From a practical usability point of view, even close rational approximations to real algebraic numbers may lead to significant errors when evaluating polyno￾mials. To see why this is so, consider the conjunction of the following polynomial constraints on input variable x and output variables y1 and y2: y 20 2 − y 2 1 .y19 2 + c18.y18 2 + · · · + c1.y2 + c0 = 0, (1) y2 > 19, y2 ≤ 20, … view at source ↗
read the original abstract

We study the problem of synthesizing programs from nonlinear real arithmetic (NRA) specifications. Existing techniques, such as syntax-guided synthesis (SyGuS), fail to synthesize programs when the specification is unrealizable. We argue this is unsatisfactory in many situations, and aim to synthesize programs from arbitrary NRA specifications, such that for any input, the synthesized program either produces outputs satisfying the specification or reports non-existence of any such output. To avoid rounding errors inherent in floating-point arithmetic, we restrict our programs to work on rational inputs and outputs. We first show that our variant of the synthesis problem is as hard as a long-standing open problem in number theory, and that synthesizing loop-free programs from arbitrary NRA specifications with rational inputs and outputs is impossible in general. Second, we present a sound and complete synthesis algorithm for the case where the specification involves a single output variable. We also show that for realizable specifications, a program generated by SyGuS for NRA (real inputs and outputs) serves as a solution to our problem, where inputs and outputs are rationals. Third, we provide a sound (but necessarily incomplete) synthesis algorithm for the general case of specifications. We have implemented our approach in a prototype tool called NQSynth that solves many benchmarks beyond the reach of state-of-the-art SyGuS tools, even when we render the specifications realizable.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper studies synthesis of programs from nonlinear real arithmetic (NRA) specifications over rational inputs/outputs, requiring the program to either produce a satisfying output or report non-existence. It proves the problem is as hard as an open number-theory question and that loop-free synthesis is impossible in general; presents a sound-and-complete algorithm for single-output specifications; shows that SyGuS solutions for realizable NRA specs over reals can be reused for the rational case; gives a sound but incomplete algorithm for the general case; and evaluates an implementation (NQSynth) that solves benchmarks beyond current SyGuS tools.

Significance. If the single-output algorithm is effective and the hardness result is tight, the work would meaningfully extend synthesis beyond realizability assumptions while staying inside rational arithmetic. The implementation and benchmark results constitute a concrete strength, as does the explicit reduction to an external open problem rather than an ad-hoc limitation.

major comments (2)
  1. [Abstract] Abstract: the soundness-and-completeness claim for the single-output case requires an effective decision procedure for NRA satisfiability over the rationals. The manuscript's own hardness reduction ties the general problem to an open question in number theory; without an explicit argument showing why the single-output fragment escapes this status (or a reduction that stays inside a known decidable fragment), the completeness claim is not yet supported.
  2. [Abstract] Abstract: the manuscript asserts soundness for the general-case algorithm and soundness/completeness for the single-output case, yet supplies no derivation, proof sketch, or error analysis for these claims. Because the central contribution is the existence of these algorithms, the absence of supporting reasoning is load-bearing.
minor comments (1)
  1. [Abstract] The abstract could more explicitly distinguish the single-output algorithm from the general-case algorithm and from the SyGuS reduction, to help readers locate the novel technical content.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and constructive feedback on the abstract. We agree that the claims regarding soundness and completeness require explicit justification and supporting reasoning, which we will add in the revision.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the soundness-and-completeness claim for the single-output case requires an effective decision procedure for NRA satisfiability over the rationals. The manuscript's own hardness reduction ties the general problem to an open question in number theory; without an explicit argument showing why the single-output fragment escapes this status (or a reduction that stays inside a known decidable fragment), the completeness claim is not yet supported.

    Authors: We agree that the abstract does not explicitly distinguish why the single-output fragment admits a complete algorithm. The full paper (Section 4) presents an algorithm that reduces single-output synthesis to a finite number of NRA satisfiability checks over Q, each involving only a single existentially quantified output variable; this fragment is handled by a decision procedure based on quantifier elimination for the existential theory of the reals (which remains effective when restricted to one output). The hardness reduction in Section 3 applies only to the multi-output case, which can encode arbitrary Diophantine equations. We will revise the abstract to include a one-sentence justification of this separation and add a short paragraph in Section 4 with the reduction details. revision: yes

  2. Referee: [Abstract] Abstract: the manuscript asserts soundness for the general-case algorithm and soundness/completeness for the single-output case, yet supplies no derivation, proof sketch, or error analysis for these claims. Because the central contribution is the existence of these algorithms, the absence of supporting reasoning is load-bearing.

    Authors: The referee is correct that the abstract provides no derivation or sketch. The body contains the full algorithms and proofs (Sections 4 and 5), but we acknowledge the abstract should convey the high-level reasoning. We will revise the abstract to include a brief outline: for the single-output case, completeness follows from exhaustive enumeration of candidate rational functions up to a degree bound derived from the specification, combined with a decision procedure for the resulting NRA queries; soundness of the general algorithm follows from a conservative over-approximation of non-realizability via interval arithmetic and Gröbner bases, with incompleteness explicitly noted due to the open hardness result. A short error analysis for the general case will also be added. revision: yes

Circularity Check

0 steps flagged

No circularity; claims reduce to external open problem rather than self-reference

full rationale

The paper explicitly reduces the general synthesis problem's hardness to a long-standing open question in number theory and states that loop-free synthesis is impossible in general, while presenting the single-output algorithm as a new construction whose completeness depends on an external (undecided) NRA satisfiability oracle over Q. No equations or steps equate a derived result to its own inputs by construction, no fitted parameters are relabeled as predictions, and no load-bearing self-citations or uniqueness theorems from the authors' prior work are invoked. The SyGuS reduction for realizable cases is presented as an independent observation rather than a definitional loop. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard decidability results for nonlinear real arithmetic and reduces general hardness to an external open problem in number theory; no free parameters or invented entities are introduced.

axioms (2)
  • standard math Satisfiability of nonlinear real arithmetic formulas over the reals is decidable
    Implicitly required for the synthesis algorithms to check realizability or find solutions in the single-output and general cases.
  • domain assumption The synthesis problem reduces to a long-standing open problem in number theory
    Used to establish that synthesizing loop-free programs from arbitrary NRA specifications is impossible in general.

pith-pipeline@v0.9.1-grok · 5787 in / 1374 out tokens · 53797 ms · 2026-06-30T13:54:34.673737+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

58 extracted references · 11 canonical work pages · 1 internal anchor

  1. [1]

    ´Abrah´ am, E., Davenport, J.H., England, M., Kremer, G.: Deciding the consis- tency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Log. Algebraic Methods Program.119(2021)

    2021

  2. [2]

    In: LPAR

    Akshay, S., Chakraborty, S., Goharshady, A.K., Govind, R., Motwani, H.J., Varanasi, S.T.: Automated synthesis of decision lists for polynomial specifications over integers. In: LPAR. EPiC Series in Computing, vol. 100, pp. 484–502. Easy- Chair (2024)

    2024

  3. [3]

    In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol

    Alur, R., Bod´ ık, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communicatio...

    2015

  4. [4]

    In: FMCAD

    Alur, R., Bod´ ık, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD. pp. 1–8 (2013)

    2013

  5. [5]

    Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM61(12), 84–93 (2018)

    2018

  6. [6]

    Akshay, S

    Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., N¨ otzli, A., Ozdemir, A., Preiner, M., 18 S. Akshay, S. Chakraborty, R. Govind and A. R. Joshi Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and...

    work page doi:10.1007/978-3-030-99524-9_24 2022

  7. [7]

    Springer Berlin, Heidelberg (2006)

    Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Springer Berlin, Heidelberg (2006)

    2006

  8. [8]

    Brown, C.W.: Improved projection for cylindrical algebraic decomposition. J. Symb. Comput.32(5), 447–465 (2001)

    2001

  9. [9]

    Chen, C., Maza, M.M.: Quantifier elimination by cylindrical algebraic decomposi- tion based on regular chains. J. Symb. Comput.75, 74–93 (2016)

    2016

  10. [10]

    In: Proceedings of the International Congress of Mathematicians

    Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians. pp. 23–35 (1962)

    1962

  11. [11]

    Code with C: Mastering rational root theorem: A practical guide (2024),https:// www.codewithc.com/mastering-rational-root-theorem-a-practical-guide/

    2024

  12. [12]

    In: Brakhage, H

    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. Springer Berlin Heidelberg (1975)

    1975

  13. [13]

    In: Caviness, B.F., Johnson, J.R

    Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition — twenty years of progress. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elim- ination and Cylindrical Algebraic Decomposition. Springer Vienna (1998)

    1998

  14. [14]

    In: SYMSACC

    Collins, G.E., Akritas, A.G.: Polynomial real root isolation using descarte’s rule of signs. In: SYMSACC. pp. 272–275. ACM (1976)

    1976

  15. [15]

    Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput.12(3), 299–328 (1991)

    1991

  16. [16]

    diophantine equations: positive aspects of a negative solution

    Davis, M., Matijasevic, Y., Robinson, J.: Hilbert’s tenth problem. diophantine equations: positive aspects of a negative solution. In: Proceedings of symposia in pure mathematics. vol. 28, pp. 323–378 (1976)

    1976

  17. [17]

    Dorato, P., Yang, W., Abdallah, C.T.: Robust multi-objective feedback design by quantifier elimination. J. Symb. Comput.24(2), 153–159 (1997)

    1997

  18. [18]

    Transactions of the American Mathematical Society369(11), pp

    Eisentr¨ aeger, K., Miller, R., Park, J., Shlapentokh, A.: As easy asQ: Hilbert’s tenth problem for subrings of the rationals and number fields. Transactions of the American Mathematical Society369(11), pp. 8291–8315 (2017)

    2017

  19. [19]

    Field, J.V.: The historical roots of elementary mathematics. lucas n. h. bunt, phillip s. jones, jack d. bedient. Isis69(2), 274–274 (1978).https://doi.org/10.1086/ 352020

    1978

  20. [20]

    Formal Methods Syst

    Fisman, D., Singh, R., Solar-Lezama, A.: Special issue on syntax-guided synthesis preface. Formal Methods Syst. Des.58(3), 469–470 (2021)

    2021

  21. [21]

    CoRRabs/2209.03602(2022)

    Goharshady, A.K., Hitarth, S., Mohammadi, F., Motwani, H.J.: Template-based program synthesis using stellens¨ atze. CoRRabs/2209.03602(2022)

    work page arXiv 2022

  22. [22]

    Goharshady, A.K., Hitarth, S., Mohammadi, F., Motwani, H.J.: Algebro-geometric algorithms for template-based synthesis of polynomial programs. Proc. ACM Pro- gram. Lang.7(OOPSLA1), 727–756 (2023)

    2023

  23. [23]

    ACM Computing Surveys23(1), 5–48 (1991).https://doi.org/10

    Goldberg, D.: What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys23(1), 5–48 (1991).https://doi.org/10. 1145/103162.103163

    work page arXiv 1991

  24. [24]

    Hong, H., Liska, R., Steinberg, S.L.: Testing stability by quantifier elimination. J. Symb. Comput.24(2), 161–187 (1997) Program Synthesis forNRA: Going Beyond Realizability 19

    1997

  25. [25]

    Reconciling Enumerative and Symbolic Search in Syntax-Guided Synthesis

    Huang, K., Qiu, X., Tian, Q., Wang, Y.: Reconciling enumerative and symbolic search in syntax-guided synthesis. CoRRabs/1802.04428(2018)

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  26. [26]

    In: Graduate texts in mathematics (1982),https://api.semanticscholar.org/ CorpusID:117927943

    Ireland, K., Rosen, M.I.: A classical introduction to modern number theory. In: Graduate texts in mathematics (1982),https://api.semanticscholar.org/ CorpusID:117927943

    1982

  27. [27]

    Jirstrand, M.: Nonlinear control system design by quantifier elimination. J. Symb. Comput.24(2), 137–152 (1997)

    1997

  28. [28]

    In: IJCAR

    Jovanovic, D., de Moura, L.M.: Solving non-linear arithmetic. In: IJCAR. pp. 339– 354 (2012)

    2012

  29. [29]

    and now for real! In: ISSAC

    Kobel, A., Rouillier, F., Sagraloff, M.: Computing real roots of real polynomials ... and now for real! In: ISSAC. pp. 303–310. ACM (2016)

    2016

  30. [30]

    Kremer, G., ´Abrah´ am, E.: Fully incremental cylindrical algebraic decomposition. J. Symb. Comput.100, 11–37 (2020)

    2020

  31. [31]

    In: PLDI

    Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI. pp. 316–329. ACM (2010)

    2010

  32. [32]

    Software Tools for Technology Transfer14(1), 1– 22 (2012).https://doi.org/10.1007/s10009-011-0217-7,https://doi.org/ 10.1007/s10009-011-0217-7

    Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for lin- ear arithmetic and sets. Software Tools for Technology Transfer14(1), 1– 22 (2012).https://doi.org/10.1007/s10009-011-0217-7,https://doi.org/ 10.1007/s10009-011-0217-7

    work page doi:10.1007/s10009-011-0217-7 2012

  33. [33]

    Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput.32(3), 231–253 (2001)

    2001

  34. [34]

    Theoretical Computer Science410(20), 1839–1850 (2009).https://doi.org/10.1016/j.tcs.2009.04.039,https://doi

    Lazard, S.: Real root isolation: A survey. Theoretical Computer Science410(20), 1839–1850 (2009).https://doi.org/10.1016/j.tcs.2009.04.039,https://doi. org/10.1016/j.tcs.2009.04.039

    work page doi:10.1016/j.tcs.2009.04.039 2009

  35. [35]

    McCallum, S.: Solving polynomial strict inequalities using cylindrical algebraic decomposition. Comput. J.36(5), 432–438 (1993)

    1993

  36. [36]

    Electronic Proceedings of the IMACS ACA (1995)

    McCallum, S.: Partial solution of a path finding problem using the cad method. Electronic Proceedings of the IMACS ACA (1995)

    1995

  37. [37]

    In: ISSAC

    McCallum, S.: On projection in cad-based quantifier elimination with equational constraint. In: ISSAC. pp. 145–149. ACM (1999)

    1999

  38. [38]

    In: ISSAC

    McCallum, S.: On propagation of equational constraints in cad-based quantifier elimination. In: ISSAC. pp. 223–231. ACM (2001)

    2001

  39. [39]

    Theoretical Computer Science507, 38– 56 (2013).https://doi.org/10.1016/j.tcs.2013.05.035,https://doi.org/10

    McCullum, J., Tiwari, P.: Lower bounds for cylindrical algebraic decomposition and applications to quantifier elimination. Theoretical Computer Science507, 38– 56 (2013).https://doi.org/10.1016/j.tcs.2013.05.035,https://doi.org/10. 1016/j.tcs.2013.05.035

    work page doi:10.1016/j.tcs.2013.05.035 2013

  40. [40]

    In: Buchberger, B., Collins, G.E., Loos, R., Albrecht, R

    Mignotte, M.: Some useful bounds. In: Buchberger, B., Collins, G.E., Loos, R., Albrecht, R. (eds.) Computer Algebra: Symbolic and Algebraic Computation, pp. 259–263. Computing Supplementa, Springer Vienna, 2 edn. (1983).https://doi. org/10.1007/978-3-7091-7551-4

    work page doi:10.1007/978-3-7091-7551-4 1983

  41. [41]

    Monniaux, D.: Quantifier elimination by lazy model enumeration. In: CAV. Lecture Notes in Computer Science, vol. 6174, pp. 585–599. Springer (2010)

    2010

  42. [42]

    Mathematics of Computation 47(175), 265–273 (1986)

    Mosier, R.G.: Root neighborhoods of a polynomial. Mathematics of Computation 47(175), 265–273 (1986)

    1986

  43. [43]

    In: TACAS

    de Moura, L.M., Bjørner, N.S.: Z3: an efficient SMT solver. In: TACAS. pp. 337–

  44. [44]

    Lecture Notes in Computer Science, Springer (2008)

    2008

  45. [45]

    Preiner, M., Schurr, H.J., Barrett, C., Fontaine, P., Niemetz, A., Tinelli, C.: Smt-lib release 2024 (incremental benchmarks) (May 2024).https://doi.org/10.5281/ zenodo.11186591,https://doi.org/10.5281/zenodo.11186591

    work page doi:10.5281/zenodo.11186591 2024

  46. [46]

    Proceedings of the American Mathematical Society10(6), 950–957 (1959) 20 S

    Robinson, J.: The undecidability of algebraic rings and fields. Proceedings of the American Mathematical Society10(6), 950–957 (1959) 20 S. Akshay, S. Chakraborty, R. Govind and A. R. Joshi

    1959

  47. [47]

    ACM Commun

    Sadeghimanesh, A., England, M.: An SMT solver for non-linear real arithmetic inside maple. ACM Commun. Comput. Algebra56(2), 76–79 (2022)

    2022

  48. [48]

    In: Proceedings of the ACM SIGPLAN 2005 Con- ference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005

    Solar-Lezama, A., Rabbah, R.M., Bod´ ık, R., Ebcioglu, K.: Programming by sketch- ing for bit-streaming programs. In: Proceedings of the ACM SIGPLAN 2005 Con- ference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005. pp. 281–294 (2005)

    2005

  49. [49]

    https://gmplib.org/(2000), accessed: 2025-02-01

    Stewart, T., Dupont, E.: The gnu multiple precision arithmetic library (gmp). https://gmplib.org/(2000), accessed: 2025-02-01

    2000

  50. [50]

    Strzebonski, A.W.: Solving systems of strict polynomial inequalities. J. Symb. Comput.29(3), 471–480 (2000)

    2000

  51. [51]

    McKinsey

    Tarski, A.: A Decision Method for Elementary Algebra and Geometry: Prepared for Publication with the Assistance of J.C.C. McKinsey. RAND Corporation, Santa Monica, CA (1951)

    1951

  52. [52]

    The Sage Developers: SageMath, the Sage Mathematics Software System (Version 10.2) (2023),https://www.sagemath.org

    2023

  53. [53]

    Proceedings of the London Mathematical Society42(2), 230–265 (1936).https://doi.org/10.1112/plms/s2-42.1.230

    Turing, A.M.: On computable numbers, with an application to the entschei- dungsproblem. Proceedings of the London Mathematical Society42(2), 230–265 (1936).https://doi.org/10.1112/plms/s2-42.1.230

    work page doi:10.1112/plms/s2-42.1.230 1936

  54. [54]

    McGraw-Hill (1948)

    Uspensky, J.V.: Theory of Equations. McGraw-Hill (1948)

    1948

  55. [55]

    Math- ematics of Computation27(123), 359–369 (1973).https://doi.org/ 10.1090/S0025-5718-1973-0337792-1,https://doi.org/10.1090/ S0025-5718-1973-0337792-1

    Vincent, R.: The roots of polynomials with real coefficients. Math- ematics of Computation27(123), 359–369 (1973).https://doi.org/ 10.1090/S0025-5718-1973-0337792-1,https://doi.org/10.1090/ S0025-5718-1973-0337792-1

    work page doi:10.1090/s0025-5718-1973-0337792-1 1973

  56. [56]

    Weispfenning, V.: Semilinear motion planning in REDLOG. Appl. Algebra Eng. Commun. Comput.12(6), 455–475 (2001)

    2001

  57. [57]

    Wikipedia: Real-root isolation — Wikipedia, the free encyclopedia (2023),https: //en.wikipedia.org/wiki/Real-root_isolation

    2023

  58. [58]

    enter numerator and denominator of ˆx:

    Wilkinson, J.H.: The evaluation of the zeros of ill-conditioned polynomials. part i. Numerische Mathematik1, 150–166 (1959) Program Synthesis forNRA: Going Beyond Realizability 21 A Appendix for Section 1 A.1 Stability Challenge for reals Consider the specificationφ(x, y) = 16≤x 2 +y 2 ≤25, whereyis an input and xis an output, and the goal is to synthesiz...

    1959