I received the following output twice using Reduce (Free CSL version), 18-Dec-09:
***** CATASTROPHIC ERROR *****
("gcdf failed" (abs omega_ac) (times (abs omega_ac) omega_ac))
***** Please report output and input listing on the sourceforge bug tracker
I was attempting to use the redlog package. The input can be written as
load_package "redlog"$ rlset R$ on rlposden$ % set up redlog
% set up conjecture
hmm := ex(theta_aa,ex(theta_bb,ex(theta_cc,ex(theta_dd,omega_ab + 1 > 0 and omega_ac +
1 > 0 and omega_ad + 1 > 0 and omega_bc + 1 > 0 and omega_bd + 1 > 0 and
omega_cd + 1 > 0 and omega_ab - 1 < 0 and omega_ac - 1 < 0 and omega_ad - 1 < 0
and omega_bc - 1 < 0 and omega_bd - 1 < 0 and omega_cd - 1 < 0 and theta_aa > 0
and theta_bb > 0 and theta_cc > 0 and theta_dd > 0 and theta_aa - 1 < 0 and
theta_bb - 1 < 0 and theta_cc - 1 < 0 and theta_dd - 1 < 0 and - omega_ab**2 +
theta_aa*theta_bb - theta_aa - theta_bb + 1 > 0 and - omega_ac**2 + theta_aa*
theta_cc - theta_aa - theta_cc + 1 > 0 and - omega_ad**2 + theta_aa*theta_dd -
theta_aa - theta_dd + 1 > 0 and 2*sqrt(omega_ab**2*omega_ac**2 - omega_ab**2 -
omega_ac**2 + 1)*sqrt( - theta_cc + 1)*sqrt( - theta_bb + 1)*omega_ab*omega_ac*
omega_bc + 2*sqrt( - theta_cc + 1)*sqrt( - theta_bb + 1)*omega_ab**2*omega_ac**2
- 2*sqrt(omega_ab**2*omega_ac**2 - omega_ab**2 - omega_ac**2 + 1)*omega_ab*
omega_ac*omega_bc - omega_ab**2*omega_ac**2*omega_bc**2 - omega_ab**2*omega_ac**
2 + omega_ab**2*omega_bc**2 - omega_ab**2*theta_bb*theta_cc + omega_ab**2*
theta_bb + omega_ab**2*theta_cc - omega_ab**2 + omega_ac**2*omega_bc**2 -
omega_ac**2*theta_bb*theta_cc + omega_ac**2*theta_bb + omega_ac**2*theta_cc -
omega_ac**2 - omega_bc**2 + theta_bb*theta_cc - theta_bb - theta_cc + 1 = 0))))$
rlqe hmm; % causes error
Thank you,
Ben
Thomas Sturm
2010-03-07
Thomas Sturm
2010-03-07
Real quantifier elimination in Redlog works exclusively over ring operations as admissible functions. The use of sqrt for the square root violates this. Within a formula any occurrence ...sqrt(ARG)... can be equivalently replaced by ex(new_var,new_var >= 0 and new_var^2 = ARG and ....new_var...). There is a procedure rlresolve, which automatically does such transformations. That is
hmm := rlresolve hmm$
before quantifier elimination will resolve the problem.
It might be considered a bug that the system does not complain about the sqrt. I will think about this. Notice that it is generally admissible to use algebraic operators like sin(x) inside formulas. These are treated like variables, i.e., the x inside the scope of sin has nothing to do with other x inside the formula. This behaviour is desired and supports the readable formulation of certain problems. In the particular case of sqrt this collides, however, with some built-in rules about sqrt.
After resolving this problem, I found that your quantifier elimination will probably not terminate within reasonable time and space. If you would like to discuss and exchange ideas about more suitable formulations, feel free to contact me.
Thomas