Abstract
At a deep level, the problems which SMT's Nonlinear Real Arithmetic (NRA) and Computer Algebra's Cylindrical Algebraic Decomposition (CAD) wish to solve are the same: nevertheless the approaches are completely different, and are described in different languages. We give an NRA/CAD dictionary, explain the CAD process as it is traditionally presented (and some variants), then ask how NRA and CAD might have a more fruitful dialogue.
| Original language | English |
|---|---|
| Journal | CEUR Workshop Proceedings |
| Volume | 1889 |
| Publication status | Published - 2017 |
ASJC Scopus subject areas
- General Computer Science