#11309: Sage sees -x +y > 0, -y + x >= 0, and x -y > 0 as equivalent
---------------------------------------------------+------------------------
Reporter: tnv | Owner: burcin
Type: defect | Status:
needs_work
Priority: major | Milestone:
sage-4.7.1
Component: symbolics | Keywords:
inequality equality relational sd31 __richcmp__
Work_issues: | Upstream: N/A
Reviewer: Karl-Dieter Crisman, ThanhVu Nguyen | Author: Keshav
Kini, Burcin Erocal
Merged: | Dependencies:
---------------------------------------------------+------------------------
Comment(by tnv):
> Which prover are you thinking of? What would this let us do in Sage?
Perhaps you should write a message to sage-devel about this.
I am thinking about the optional package too. Someone told me qepcad (not
exactly SMT but can be used for many similar purpose) already in Sage as
an optional package.
The good thing about these SMT solvers is that most of them support a
standard language (smtlib) and therefore you can use any of the SMT's out
there with a single interface. SMT can be used to show if something (a
set of expressions or constraints) is valid or satisfiable under
different types of theories (not just boolean), or simplify a set of
expression, etc. I rely on these for implications on my project-- to see
if 2 sets of expressions are equi-satisfiable .
So all the above examples of whether if exp1 == exp2 should be easily
answered with SMT.
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/11309#comment:31>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sage-trac?hl=en.
