Solving quantified formulas (quantifier elimination)

[jarble]

It might be useful to extend the computational-algebra library to solve quantified formulas instead of quantifier-free formulas.

I found a Haskell library that eliminates quantifiers formulas using cylindrical algebraic decomposition: could this library be used to solve quantified formulas in computational-algebra?

[konn]

Thank you for your suggestion!

When talking about Quantifier Elimination, you should specify the theory in which you want to do QE; since you mentioned CAD, I assume you are talking about QE over Real Closed Field.

I'm not familiar with the package you pointed out, but it seems less typed (i.e. does not provide a way to distinguish polynomial rings with different sets variables at type-level), we need some glue code to make it work with our library. It might be easier to translate our polynomials into qepcad's one and then (unsafely) cast back.

As an alternative solution, you can directly implement CAD on top computational-algebra package. Indeed, Strum-Habicht sequence, one of a fundamental building block of CAD algorithm, is already present in the computational-algebra package. We use it to real root isolation in implementing algebraic reals.

I think both approaches can make sense. Patches welcome!