More Web Proxy on the site http://driver.im/

research-article

Reduction of Transcendental Decision Problems over the Reals

Authors:

Bican XiaAuthors Info & Claims

ISSAC '24: Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation

Pages 56 - 64

https://doi.org/10.1145/3666000.3669675

Published: 16 July 2024 Publication History

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.

Digital Library

[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.

Digital Library

[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

Digital Library

[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.

Digital Library

[7]

Bobby Forrester Caviness. 1970. On canonical forms and simplification. Journal of the ACM (JACM) 17, 2 (1970), 385–396.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[27]

Adam Strzeboński. 2011. Cylindrical decomposition for systems transcendental in the first variable. Journal of Symbolic Computation 46, 11 (2011), 1284–1290.

Digital Library

[28]

Adam Strzeboński. 2012. Real root isolation for exp–log–arctan functions. Journal of Symbolic Computation 47, 3 (2012), 282–314.

Digital Library

[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.

Digital Library

[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.

Digital Library

Cited By

Lipparini ERatschan S(2025)Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search ProblemJournal of Automated Reasoning10.1007/s10817-024-09716-369:1Online publication date: 25-Jan-2025
https://doi.org/10.1007/s10817-024-09716-3
Ni XXia BZhao T(2024)Local Search for Checking Satisfiability of Formulas with Trigonometric FunctionsAutomated Technology for Verification and Analysis10.1007/978-3-031-78750-8_13(256-274)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-78750-8_13

Index Terms

Reduction of Transcendental Decision Problems over the Reals
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms

Recommendations

Deciding first-order formulas involving univariate mixed trigonometric-polynomials
ISSAC '23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation

A 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

cover image ACM Conferences

ISSAC '24: Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation

July 2024

470 pages

ISBN:9798400706967

DOI:10.1145/3666000

Editors:
Jonathan Hauenstein
University of Notre Dame, USA
,
Wen-shin Lee
University of Stirling, UK
,
Shaoshi Chen
Chinese Academy of Sciences, China

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

SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 July 2024

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

National Key R&D Program of China

Conference

ISSAC '24

Sponsor:

SIGSAM

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

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
79
Total Downloads

Downloads (Last 12 months)79
Downloads (Last 6 weeks)9

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lipparini ERatschan S(2025)Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search ProblemJournal of Automated Reasoning10.1007/s10817-024-09716-369:1Online publication date: 25-Jan-2025
https://doi.org/10.1007/s10817-024-09716-3
Ni XXia BZhao T(2024)Local Search for Checking Satisfiability of Formulas with Trigonometric FunctionsAutomated Technology for Verification and Analysis10.1007/978-3-031-78750-8_13(256-274)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-78750-8_13

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Figures

Tables

Media

View Table of Conten