Revision history [back]

One possible approach could be to use qepcad optional package. You can install it by typing from a terminal:

sage -i qepcad

Then, you can do something:

sage: var('t')
t
sage: qf = qepcad_formula
sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2 > 0))
sage: f
(A t)[[t > 0 /\ t < 1/2] ==> (t^2 - 1)/(t^2 - 3) + 4 > 0]
sage: qepcad(f)

But apparently, it takes too much time. So, if only the sign matters, you can notice that the sign of a/b is the same than the one of a*b, so, up to taking care of the possible cases when b=0, you can do:

sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2.denominator()*expr2.numerator() > 0))
sage: qepcad(f)
TRUE

Which is correct.

One possible approach could be to use qepcad optional package. You can install it by typing from a terminal:

sage -i qepcad

Then, you can do something:

sage: var('t')
t
sage: qf = qepcad_formula
sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2 > 0))
sage: f
(A t)[[t > 0 /\ t < 1/2] ==> (t^2 - 1)/(t^2 - 3) + 4 > 0]
sage: qepcad(f)

But apparently, it takes too much time. So, if only the sign matters, you can notice that the sign of a/b is the same than the one of a*b, so, up to taking care of the possible cases when b=0, you can do:

sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2.denominator()*expr2.numerator() > 0))
sage: qepcad(f)
TRUE

Which is correct.

One possible approach could be to use qepcad optional package. You can install it by typing from a terminal:

sage -i qepcad

Then, you can do something:

sage: var('t')
t
sage: qf = qepcad_formula
sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2 > 0))
sage: f
(A t)[[t > 0 /\ t < 1/2] ==> (t^2 - 1)/(t^2 - 3) > 0]
sage: qepcad(f)

But apparently, it takes too much time. time (unless qepcad is only able do deal with polynomials but the interface does not catch the error, to be investigated). So, if only the sign matters, you can notice that the sign of a/b is the same than the one of a*b, so, up to taking care of the possible cases when b=0, you can do:

sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2.denominator()*expr2.numerator() > 0))
sage: qepcad(f)
TRUE

Which is correct.

One possible approach could be to use qepcad optional package. You can install it by typing from a terminal:

sage -i qepcad

Then, you can do something:

sage: var('t')
t
sage: qf = qepcad_formula
sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2 > 0))
sage: f
(A t)[[t > 0 /\ t < 1/2] ==> (t^2 - 1)/(t^2 - 3) > 0]
sage: qepcad(f)

But apparently, it takes too much time (unless qepcad is only able do deal with polynomials but the interface does not catch the error, to be investigated). So, if only the sign matters, you can notice that the sign of a/b is the same than the one of a*b, so, up to taking care of the possible cases when b=0, you can do:

sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2.denominator()*expr2.numerator() > 0))
sage: qepcad(f)
TRUE

Which is correct.

sage: qepcad(f) == 'TRUE'
True

sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2.denominator()*expr2.numerator() <= 0))
sage: qepcad(f) == 'TRUE'
False