How do I make assume conclude basic consequences?

[Rob H.]

Hi,

I have

sage: var('A,B')

sage: assume(A>1)

sage: assume(B>A)

sage: bool(2*B>A)

False

Now, I know it's that sage considers 2*B and A incomparable, not that it actually thinks that 2*B <= A. And similarly,

sage: bool(B > A - 10)

False

Is this really something sage (i.e. maxima) can't handle? Is there some trick I can use without manually assuming each such case that arises?

Thanks,

Rob

[Ralf Stephan]

On Saturday, October 8, 2016 at 12:14:23 PM UTC+2, Rob H. wrote:

sage: var('A,B')

sage: assume(A>1)

sage: assume(B>A)

sage: bool(2*B>A)

False

Maxima 5.37.2:

(%i1) assume(a>1);

(%o1)                               [a > 1]

(%i2) assume(b>a);

(%o2)                               [b > a]

(%i3) is(2*b>a);

(%o3)                               unknown

 

SymPy:

In [4]: ask(Q.is_true(2*y>x), Q.is_true(x>1) & Q.is_true(y>x))

In [5]:

There is no SMT solver capability in Sage, nor its subsystems.

I know there are plans for this in SymPy. Plans we have too:

https://trac.sagemath.org/ticket/19162

Regards,

[bernardp...@gmail.com]

There is no advanced algorithm to do that in giac, but for simple examples like that it works:
assume(a>1); assume(b>a); 2b>a;

[slelievre]

You might want to use QEPCAD.

See the documentation for Sage's interface to QEPCAD:

http://doc.sagemath.org/html/en/reference/interfaces/sage/interfaces/qepcad.html