search

konn / computational-algebra

General-Purpose Computer Algebra System as an EDSL in Haskell
http://konn.github.io/computational-algebra/
BSD 3-Clause "New" or "Revised" License
92 stars 9 forks source link

Solving quantified formulas (quantifier elimination) #10

Open jarble opened 3 years ago

jarble commented 3 years ago

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 commented 3 years ago

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!