quantifier elimination

[Jason Grout]

Is there any quantifier elimination functionality in SAGE? If not, is
there any interest in trying to incorporate QEPCAD, which uses
cylindrical algebraic decomposition to eliminate quantifiers in
statements. In other words, QEPCAD takes the statement

there exists an x such that a*x^2 + b*x + c = 0 and a /= 0

and eliminates the quantifier and answers that:

a /= 0 and 4 a c - b^2 <= 0

In other words, it gives you the conditions of a solution satisfying
your original statement.

Mathematica has such functionality and I believe that Maple does as
well. REDUCE has the functionality in the REDLOG package.

I couldn't find a license for QEPCAD, and the library that QEPCAD
depends on (SACLIB) is not GPL. However, we could ask if they would
release it under GPL for us.

References:

QEPCAD: http://www.cs.usna.edu/~qepcad/B/QEPCAD.html

REDUCE REDLOG package: http://www.algebra.fim.uni-passau.de/~redlog/

Mathematica implementation (Resolve, Reduce, FindInstance,
CylindricalDecomposition, etc.):

http://reference.wolfram.com/mathematica/tutorial/Quantifiers.html

http://reference.wolfram.com/mathematica/tutorial/TheRepresentationOfSolutionSets.html

http://reference.wolfram.com/mathematica/tutorial/Inequalities-ManipulatingEquationsAndInequalities.html

http://reference.wolfram.com/mathematica/tutorial/EquationsAndInequalitiesOverDomains.html

I've used this functionality in Mathematica to solve some problems, and
it seemed like the Mathematica implementation was more powerful than the
QEPCAD implementation (i.e., Mathematica would do problems after QEPCAD
would give up because the problem was too hard). I bring all this up
because it has been useful and cool to use this in the past and I don't
want to forget to mention it to SAGE, in case it hasn't been considered
before.

-Jason

[boo...@u.washington.edu]

Note: round these parts, we use != for inequality. /= is a divide in-place. That is:

sage: a = 4
sage: a /= 2
sage: print a
2

[David Joyner]

If there is any interest, I can ask Chris Brown, who I know fairly
well. I think I asked him about licenses once. I vaguely remember him saying
all his stuff is GPL-compatible (or even public domain) but saclib
is separate.

++++++++++++++++++++++++++++++++++++++++++++++++

[Jason Grout]

boo...@u.washington.edu wrote:
> Note: round these parts, we use != for inequality. /= is a divide in-place. That is:
>
> sage: a = 4
> sage: a /= 2
> sage: print a
> 2

ahh, right. If we wrap QEPCAD, then we'll probably have to change the
input and output, then, as it uses /= for not equals.

-Jason

[Jason Grout]

David Joyner wrote:
> If there is any interest, I can ask Chris Brown, who I know fairly
> well. I think I asked him about licenses once. I vaguely remember him saying
> all his stuff is GPL-compatible (or even public domain) but saclib
> is separate.
>

The license for SACLIB says:

"Persons or institutions receiving it are pledged not to distribute it
to others. Instead, individuals wishing to acquire the system should
obtain it by ftp directly from the Kurt Goedel Institute, informing the
Institute of the acquisition. Thereby the SACLIB Group will know who has
the system and be able to inform all users of any corrections or newer
versions."

[...]

"Neither SACLIB nor any part thereof may be incorporated in any
commercialsoftware product without the consent of the authors. Users
developing non-commercial application packages are kindly asked to
inform us."

However, in briefly glancing through the documentation to saclib, it
seems that we have (or should have) much of the same functionality
already in SAGE, so if the people in charge of saclib do not agree, it
might be feasible to replace the saclib dependency of QEPCAD with
something else. Already, there is a switch in QEPCAD that allows you to
use Singular for some computations that might be faster (or not present)
in saclib.

-Jason

[David Joyner]

I spoke with Chris Brown, who is essentially now the maintainer of
qepcad. Here is his response:

"Saclib's actual status is probably a bit up in the air. What I might
call the saclib "stakeholders" had agreed to GPL it, but everybody
was, I guess, too busy to do anything about it. Qepcad's status is
similar ... except that my contributions are necessarily public
domain."

In a second email, he added:

"If you're interested, we can talk about this. Ultimately I can ask the
saclib/qepcad folks for permission and move forward."

On 9/22/07, Jason Grout <jason...@creativetrax.com> wrote:
>

[Jason Grout]

David Joyner wrote:
> I spoke with Chris Brown, who is essentially now the maintainer of
> qepcad. Here is his response:
>
>
> "Saclib's actual status is probably a bit up in the air. What I might
> call the saclib "stakeholders" had agreed to GPL it, but everybody
> was, I guess, too busy to do anything about it. Qepcad's status is
> similar ... except that my contributions are necessarily public
> domain."
>
> In a second email, he added:
>
> "If you're interested, we can talk about this. Ultimately I can ask the
> saclib/qepcad folks for permission and move forward."

Wow, thanks! Although I brought this up, I don't have the experience to
implement a front-end (and probably shouldn't spread myself thin enough
to learn right now). I'll create a ticket for it, though, and if
someone hasn't done it already when I have more time, I'll learn how to
do it.

Thanks,

Jason

[Jason Grout]

It's ticket 772: http://trac.sagemath.org/sage_trac/ticket/772

Thanks,

Jason