Reduction of Transcendental Decision Problems over the Reals
Authors: 
Rizeng Chen, Bican XiaAuthors Info & Claims
Pages 56 - 64
Abstract
A special class of univariate transcendental decision problems called “trigonometric extension” is studied in this paper. Roughly speaking, a trigonometric extension is a ring of univariate analytic functions obtained by adjoining trigonometric functions to a ring consisting of functions having only finitely many real zeros. It is shown that in this case, the decision problem can be reduced to looking for solutions in a bounded domain. Based on the reduction, several new decidability results are established when Schanuel’s Conjecture is assumed. Furthermore, for the theory of multivariate trigonometric extension, it is proved that, although a small fragment of the theory can be reduced to the univariate case, the general theory is undecidable.
References
[1]
Melanie Achatz, Scott McCallum, and Volker Weispfenning. 2008. Deciding polynomial-exponential problems. In Proceedings of the twenty-first international symposium on Symbolic and algebraic computation. 215–222.
[2]
Hirokazu Anai and Volker Weispfenning. 2000. Deciding linear-trigonometric problems. In Proceedings of the 2000 international symposium on Symbolic and algebraic computation. 14–22.
[3]
Hirokazu Anai and Volker Weispfenning. 2001. Reach set computations using real quantifier elimination. In International Workshop on Hybrid Systems: Computation and Control. Springer, 63–76.
[4]
Vladimir I Arnold. 1992. Ordinary differential equations. Springer Science & Business Media.
[5]
Saugata Basu, Richard Pollack, and Marie-Françoise Roy. 2006. Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer-Verlag, Berlin, Heidelberg. https://perso.univ-rennes1.fr/marie-francoise.roy/bpr-ed2-posted3.html
[6]
Paul C Bell, Jean-Charles Delvenne, Raphaël M Jungers, and Vincent D Blondel. 2010. The continuous skolem-pisot problem. Theoretical Computer Science 411, 40-42 (2010), 3625–3634.
[7]
Bobby Forrester Caviness. 1970. On canonical forms and simplification. Journal of the ACM (JACM) 17, 2 (1970), 385–396.
[8]
Rizeng Chen, Haokun Li, Bican Xia, Tianqi Zhao, and Tao Zheng. 2024. Isolating all the real roots of a mixed trigonometric-polynomial. Journal of Symbolic Computation 121 (2024), 102250.
[9]
Rizeng Chen and Bican Xia. 2023. Deciding first-order formulas involving univariate mixed trigonometric-polynomials. In Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation. 145–154.
[10]
Shiping Chen and Zhong Liu. 2020. Automated proof of mixed trigonometric-polynomial inequalities. Journal of Symbolic Computation 101 (2020), 318–329.
[11]
Ventsislav Chonev, Joël Ouaknine, and James Worrell. 2016. On the Skolem Problem for Continuous Linear Dynamical Systems. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy(LIPIcs, Vol. 55), Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 100:1–100:13. https://doi.org/10.4230/LIPICS.ICALP.2016.100
[12]
Timothy Y Chow. 1999. What is a closed-form number?The American mathematical monthly 106, 5 (1999), 440–448.
[13]
George E Collins. 1975. Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In Automata Theory and Formal Languages: 2nd GI Conference Kaiserslautern, May 20–23, 1975. Springer, 134–183.
[14]
Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, and Naijun Zhan. 2015. Decidability of the reachability for a family of linear vector fields. In Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings 13. Springer, 482–499.
[15]
Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan. 2016. Computing reachable sets of linear vector fields revisited. In 2016 European Control Conference (ECC). IEEE, 419–426.
[16]
Miklós Laczkovich. 2003. The removal of π from some undecidable problems involving elementary functions. Proc. Amer. Math. Soc. 131, 7 (2003), 2235–2240.
[17]
Gerardo Lafferriere, George J Pappas, and Sergio Yovine. 2001. Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computation 32, 3 (2001), 231–253.
[18]
Serge Lang. 1966. Introduction to Transcendental Numbers. Addison-Wesley.
[19]
Angus Macintyre. 2016. Turing meets Schanuel. Annals of Pure and Applied Logic 167, 10 (2016), 901–938.
[20]
Angus Macintyre and Alex J Wilkie. 1996. On the decidability of the real exponential field. KREISEL’S MATHEMATICS 115 (1996), 451.
[21]
Yu V Matijasevič. 1973. On recursive unsolvability of Hilbert’s tenth problem. In Studies in Logic and the Foundations of Mathematics. Vol. 74. Elsevier, 89–110.
[22]
Scott McCallum and Volker Weispfenning. 2012. Deciding polynomial-transcendental problems. Journal of Symbolic Computation 47, 1 (2012), 16–31.
[23]
Daniel Richardson. 1969. Some undecidable problems involving elementary functions of a real variable. The Journal of Symbolic Logic 33, 4 (1969), 514–520.
[24]
Daniel Richardson. 1997. How to recognize zero. Journal of Symbolic Computation 24, 6 (1997), 627–645.
[25]
Adam Strzeboński. 2008. Real root isolation for exp-log functions. In Proceedings of the twenty-first international symposium on Symbolic and algebraic computation. 303–314.
[26]
Adam Strzeboński. 2009. Real root isolation for tame elementary functions. In Proceedings of the 2009 international symposium on Symbolic and algebraic computation. 341–350.
[27]
Adam Strzeboński. 2011. Cylindrical decomposition for systems transcendental in the first variable. Journal of Symbolic Computation 46, 11 (2011), 1284–1290.
[28]
Adam Strzeboński. 2012. Real root isolation for exp–log–arctan functions. Journal of Symbolic Computation 47, 3 (2012), 282–314.
[29]
A. Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press.
[30]
Paul S Wang. 1974. The undecidability of the existence of zeros of real elementary functions. Journal of the ACM (JACM) 21, 4 (1974), 586–589.
[31]
Ming Xu, Zhi-Bin Li, and Lu Yang. 2015. Quantifier elimination for a class of exponential polynomial formulas. Journal of Symbolic Computation 68 (2015), 146–168.
Index Terms
- Reduction of Transcendental Decision Problems over the Reals
Recommendations
Deciding first-order formulas involving univariate mixed trigonometric-polynomials
ISSAC '23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic ComputationA decision algorithm for the first-order theory of univariate mixed trigonometric-polynomials over the reals is proposed in this paper. In the development of the decision algorithm, the concept "contraction mapping associated with an algebraic function" ...
Explicit Solutions for Transcendental Equations
A simple method to formulate an explicit expression for the roots of any analytic transcendental function is presented. The method is based on Cauchy's integral theorem and uses only basic concepts of complex integration. One convenient method for ...
Cylindrical decomposition for systems transcendental in the first variable
We present a generalization of the Cylindrical Algebraic Decomposition (CAD) algorithm to systems of equations and inequalities in functions of the form p(x,f"1(x),...,f"m(x),y"1,...,y"n), where p@?Q[x,t"1,...,t"m,y"1,...,y"n] and f"1(x),...,f"m(x) are ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
July 2024
470 pages
Copyright © 2024 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 16 July 2024
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Funding Sources
- National Key R&D Program of China
Conference
ISSAC '24
Sponsor:
ISSAC '24: International Symposium on Symbolic and Algebraic Computation
July 16 - 19, 2024
NC, Raleigh, USA
Acceptance Rates
Overall Acceptance Rate 395 of 838 submissions, 47%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 69Total Downloads
- Downloads (Last 12 months)69
- Downloads (Last 6 weeks)5
Reflects downloads up to 01 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML Format