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
Fingerprint
Dive into the research topics of 'SMT Nonlinear Real Arithmetic and Computer Algebra: A dialogue of the deaf?'. Together they form a unique fingerprint.Cite this
- APA
- Standard
- Harvard
- Vancouver
- Author
- BIBTEX
- RIS