Revision history [back]

Your question is a bit daunting, but let us make some experiments (Sage predefines x to be a global indeterminate):

sage: p=x^2+2*x-3
sage: p.parent()
Symbolic Ring

Who is this guy? His nickname is SR:

sage: SR?
Symbolic Ring, parent object for all symbolic expressions.

One of the main goals of symbolic calculus is to solve equations:

sage: solve(p==0,x), solve(p==1,x)
([x == -3, x == 1], [x == -sqrt(5) - 1, x == sqrt(5) - 1])

Assume is badly documented, but looks useful in this context:

sage: assume(x>0)
sage: solve(p==0,x), solve(p==1,x)
([x == 1], [x == sqrt(5) - 1])
sage: assume(x, 'rational')
sage: assumptions()
[x > 0, x is rational]
sage: solve(p==0,x), solve(p==1,x)
([x == 1], [])

So far so good, and back to your question: is Sage a proof checker, which could help to check derivation of new propositions from assumptions? Answer is definitely negative:

sage: forget(); assume(p==0); assumptions()
[x^2 + 2*x - 3 == 0]
sage: prop = (x==1) or (x==-3); prop
x == -3

This very strange result is explained in a preceeding post.

sage: bool (prop)
False

Imho, no hope for improving your function, Sage is not the right tool. If you are interested in proof checkers, take a look at Coq, but this is another story.