# Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

Function Repository Resource:

Prove or disprove a closed first-order formula in the theory of univariate mixed trigonometric polynomials

Contributed by:
Rizeng Chen (xiaxueqaq)

ResourceFunction["VerifyMTP"][ returns the truth value of a |

A mixed trigonometric polynomial expression is often referred to as an MTP.

The input *formula* must be a closed (i.e. fully quantified) formula in the first order theory of univariate mixed trigonometric polynomials. Since there is only one variable in this theory, a legal input should be a ForAll or Exists quantified expression.

Only univariate mixed trigonometric polynomials with rational and/or integer coefficients are allowed in *formula*, and all denominators should be cleared. That is to say, the input should a polynomial in the variable itself or sines and/or cosines of the variable.

Prove that if *x* is a positive solution to *x*^{2}=*tanx*, then *x*>1:

In[1]:= |

Out[1]= |

Verify a formula in the first order theory of MTPs:

In[2]:= |

Out[2]= |

Verify a complicated example:

In[3]:= |

Out[3]= |

Prove MTP inequalities:

In[4]:= |

Out[4]= |

Show that is a point on the curve given by *x*=*sin t*, *y*=*sin** *2*t* by finding an explicit value for *t*:

In[5]:= |

Out[5]= |

When *x* is bounded, Reduce can be used:

In[6]:= |

Out[6]= |

In[7]:= |

Out[7]= |

When *x* is unbounded, Reduce is not able to give a result:

In[8]:= |

Out[8]= |

VerifyMTP handles this input however:

In[9]:= |

Out[9]= |

Show that the circle 25*x*^{2}+25(*y*-3)^{2}=36 is disjoint from the parametric curve *x*=*t**cos*^{2}*t*, *y*=*t sin t*:

In[10]:= |

Out[10]= |

Note that it is very hard to tell from a plot if the two curves are disjoint:

In[11]:= |

Out[11]= |

- Scott McCallum, Volker Weispfenning - Deciding polynomial-transcendental problems
- Adam Strzeboński - Real root isolation for exp-log-arctan functions
- Rizeng Chen, Bican Xia - Deciding first-order formulas involving univariate mixed trigonometric-polynomials

Wolfram Language 13.0 (December 2021) or above

- 1.0.0 – 15 December 2023

This work is licensed under a Creative Commons Attribution 4.0 International License