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.

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]
Error RPFACTREAD: Digit was expected.
(A f) (A z) [[f > 0 /\ f <= 1 /\ z >= 1/s