# Q E P C A D - Formulas

The idea here is to come up with some format for formulas that will allow me to do all the manipulations I want. Here is the definition of a formula in this format.

Let D be a CAD and P be its projection factor set:

1. (TRUE) and (FALSE) are both formulas.

2. ((i,j),op) is a formula, where 0 < i <= |P| and 0 < j <= |P_i|, and op is in {LTOP,EQOP,GTOP,GEOP,NEOP,LEOP}.

3. (ANDOP,F_1,...,F_i) is a formula, where i > 1 and F_1,...,F_i are formulas.

4. (OROP,F_1,...,F_i) is a formula, where i > 1 and F_1,...,F_i are formulas.

5. ((i,j),(op,k)) is a formula,where 0 < i <= |P| and 0 < j < |P_i|, and op is in {LTOP,EQOP,GTOP,GEOP,NEOP,LEOP} and k is a non-zero int.
The list (i,j) will refer to a polynomial in the following way: The signiture vector for a given cell assumes an ordering on the polynomials of a given level in P. So, (i,j) refers to the jth polynomial in the ordering of the elements of P_i. The interpretation of 5. is probably deserving of some explanation. Let us give a name to the polynomial (i,j), call it q(x_1, ...,x_i). Then ((i,j),(op,k)) is interpreted as
if k > 0
x_i op "the kth root of q(x_1, ..., x_{i-1}, X)", where X is a purely symbolic variable. This atomic formula is true if and only if q(x_1, ..., x_{i-1}, X) has at least k roots, and x_i bears relation op to the kth of these, ordered smallest to largest.
if 0 > k
x_i op "the |k|th root of q(x_1, ..., x_{i-1}, X)", where X is a purely symbolic variable. This atomic formula is true if and only if q(x_1, ..., x_{i-1}, X) has at least |k| roots, and x_i bears relation op to the |k|th of these, ordered largest to smallest.