SMT Nonlinear Real Arithmetic and Computer Algebra: A dialogue of the deaf?

Research output: Contribution to journalArticle

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 languageEnglish
JournalCEUR Workshop Proceedings
Volume1889
Publication statusPublished - 2017

ASJC Scopus subject areas

  • Computer Science(all)

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