# Revision history [back]

As explained in the documentation, qepcad is supposed to deal with polynomials, so it is likely it is not able to handle the square root (nor the fraction). The following works:

sage: qepcad(qf.implies(qf.and_(f>0, f<=1, z>=0, z^2*(1+4*f/5)>=1), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0))
TRUE


The main concern is that it does not raises an error when there is a square root in the formula (probably a lack of sanity checking). I will have a deeper look to the source code and tell if i found something intersting.

As explained in the documentation, qepcad is supposed to deal with polynomials, so it is likely it is not able to handle the square root (nor the fraction). The following works:

sage: qepcad(qf.implies(qf.and_(f>0, f<=1, z>=0, z^2*(1+4*f/5)>=1), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0))
TRUE


The main concern is that it does not raises an error when there is a square root in the formula (probably a lack of sanity checking). I will have a deeper look to the source code and tell if i found something intersting.interesting. Thanks for reporting anyway.

As explained in the documentation, qepcad is supposed to deal with polynomials, so it is likely it is not able to handle the square root (nor the fraction). The following works:So, a correct way to formulate your statement using qepcad would be the following:

sage: qepcad(qf.implies(qf.and_(f>0, f<=1, z>=0, z^2*(1+4*f/5)>=1), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0))
TRUE


The main concern is that it does not raises an error when there is a square root in the formula (probably a lack of sanity checking). checking and/or error handling). I will have a deeper look to the source code and tell if i found something interesting. it couls be improved. Thanks for reporting anyway.

As explained in the documentation, qepcad is supposed to deal with polynomials, so it is likely it is not able to handle the square root (nor the fraction). So, a correct way to formulate your statement using qepcad would be the following:

sage: qepcad(qf.implies(qf.and_(f>0, f<=1, z>=0, z^2*(1+4*f/5)>=1), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0))
TRUE


The main concern is that it does not raises an error when there is a square root in the formula (probably a lack of sanity checking and/or error handling). I will have a deeper look to the source code and tell if it couls could be improved. Thanks for reporting anyway.

As explained in the documentation, qepcad is supposed to deal with polynomials, so it is likely it is not able to handle the square root (nor the fraction). So, a correct way to formulate your statement using qepcad would be the following:following (note the additional z>=0 because of the square):

sage: qepcad(qf.implies(qf.and_(f>0, f<=1, z>=0, z^2*(1+4*f/5)>=1), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0))
TRUE


The main concern is that it does not raises an error when there is a square root in the formula (probably a lack of sanity checking and/or error handling). I will have a deeper look to the source code and tell if it could be improved. Thanks for reporting anyway.

As explained in the documentation, qepcad is supposed to deal with polynomials, so it is likely it is not able to handle the square root (nor the fraction). So, a correct way to formulate your statement using qepcad would be the following (note the additional z>=0 because of the square):

sage: qepcad(qf.implies(qf.and_(f>0, f<=1, z>=0, z^2*(1+4*f/5)>=1), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0))
TRUE


The main concern is that it does not raises an error when there is a square root in the formula (probably a lack of sanity checking and/or error handling). I will have a deeper look to the source code and tell if it could be improved. Thanks for reporting anyway.

EDIT

qepcad seem indeed not able to deal with the sqrt, but Sage interace does not handle the error, here is a qepcad session:

Enter a variable list:
(f,z)
Enter the number of free variables:
0
Enter a prenex formula:
(A f) (A z) [[f > 0 /\ f <= 1 /\ z >= 1/sqrt(4/5 f + 1)] ==> ((f + z)^2 - f^2 - 1)^2 + (2 f + z - 1)^2 - 4 f^2 > 0]