Program synthesis for non-linear real arithmetic: going beyond realizability

DOI10.1007/978-3-032-32589-1_15MaRDI QIDQ7411168zbMATH OpenFDO

Authors S. Akshay, Supratik Chakraborty, R. Govind, Aniruddha R. Joshi

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_15

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Algorithms in real algebraic geometry
• An SMT solver for non-linear real arithmetic inside maple
• As easy as \(\mathbb {Q}\): Hilbert's tenth problem for subrings of the rationals and number fields
• Automated synthesis of decision lists for polynomial specifications over integers
• Computing Real Roots of Real Polynomials ... and now For Real!
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Fully incremental cylindrical algebraic decomposition
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 3539209 (Why is no real title available?)
• scientific article; zbMATH DE number 1157648 (Why is no real title available?)
• scientific article; zbMATH DE number 3189696 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• Improved projection for cylindrical algebraic decomposition
• Nonlinear control system design by quantifier elimination
• On computable numbers, with an application to the Entscheidungsproblem.
• On propagation of equational constraints in CAD-based quantifier elimination
• Partial cylindrical algebraic decomposition for quantifier elimination
• Quantifier elimination by cylindrical algebraic decomposition based on regular chains
• Robust multi-objective feedback design by quantifier elimination
• Semilinear motion planning in REDLOG
• Solving non-linear arithmetic
• Solving Polynomial Strict Inequalities Using Cylindrical Algebraic Decomposition
• Solving systems of strict polynomial inequalities
• Special issue on syntax-guided synthesis preface
• Symbolic reachability computation for families of linear vector fields
• Testing stability by quantifier elimination
• The expected asymptotical ratio for preemptive stochastic online problem
• The Undecidability of Algebraic Rings and Fields
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
• Tools and algorithms for the construction and analysis of systems. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2--7, 2022. Proceedings. Pa

This page was built for publication: Program synthesis for non-linear real arithmetic: going beyond realizability

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