Problem: Given a quantifier formula  in r variables, with f free variables, containing trigonometric polynomials, compute a quantifier free formula  in f variables equivalent to .

For formulas containing algebraic polynomials, there are many methods to attack the quantifier elimination problems. Implementations of some of these methods are also available:

• Mathematica V4.0 contains an implementation of CAD (Collins' cylindrical algebraic decomposition); this algorithm does not eliminate quantifiers in a quantified formula -- given a quantifier-free formula, it computes a decomposition of the space of all variables into cells over which the polynomials are sign-invariant;
• the package qepcad of Hoon Hong (email hhong@risc.uni-linz.ac.at) implements Hoon Hong and George Collins' method of quantifier elimination by partial cylindrical algebraic decomposition;
• REDLOG is a package for quantifier elimination for formulas that contain linear polynomials and at most a second degree polynomial. It has been developped at the University of Passau, by a group under the leadership of Volker Weispfening.

Basically, this method decomposes first the space, cylindrically, into cells on which the polynomials that occur in the initial formula have constant sign. For each cell, a sample point is also provided. Once this phase is completed, an evaluation process takes place. The formula is evaluated at each sample point, after which, the evaluation process is carried iteratively, using the quantifiers, until the f-dimensional cells on which the formula is true are isolated.

We have adapted this method to the trigonometric case; a description of the algorithm, together with the background theory, can be found in RISC technical report 99-07. For experimental purposes, we have produced a partial implementation in C, built up on the package saclib.
 

Programs

  Release 1-02

• tpolqe.linux.gz
• tpolqe.irix.gz
• sources: tpolqe.tar.gz

  Release 1-01

• tpolqe.linux.gz
• tpolqe.irix.gz

Here is a sample of a run:

The input formula is equivalent to:
  [
   (x^2 - 2) > 0 /\
   (x + 1) < 0
  ]
  \/
  [
   (x^2 - 2) > 0 /\
   (x) > 0
  ]
 
>

• the list of variables must be given between paranthesis, without any blank;
• the quantifiers are given as A (for forall) and E (for exists);
• the quantifier-free part of the formula must be inserted between square brackets, and must end with period;
• do not hesitate to use square brackets whenever the precedence rules are not so obvious:

• the input syntax of the trigonometric polynomials is rather complicated:
• a trigonometric polynomial is a sum of monomials:
p = m1 + m2 + ...
• each monomial is a product of a coefficient and sines/cosines:
m = c * s1 * s2 * ...
• the coefficient is an algebraic polynomial with integer coefficients:
c = i v^e u^f + ...
• the syntax of an algebraic polynomial is:
c = t1 + t2 + ...
where each ti is a term. The order in which you gave the variables, at the beginning, is very important, as the terms should be ordered decreasingly according to this order.
• the variables should occur in a term increasingly, according to the order.
• the trigonometric functions are sines and cosine of variables:
sin(v)^e, cos(v)^v

• in the coefficients, between the variables in a term, there should be no sign, whereas between the elements of a monomial there should be "*";
• the coefficients of monomials should be put between paranthesis, even though they are integer numbers;
• the arguments of trigonometric functions are variables at the first power, without integer multipliers.

Output

• true or false, if the formula has no free variables;
• an equivalent quantifier-free formula, if the initial formula has one free variable;
• a set of f-dimensional sample points, corresponding to cells over which the initial formula is true, if f>2.

Although the program has been tested on a quite extensive set of examples, we expect that there are still some errors and bugs. If you find any, please submit a report to the address: