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

Fingerprint

Surface mount technology
Algebra
Decomposition
Glossaries

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

SMT Nonlinear Real Arithmetic and Computer Algebra : A dialogue of the deaf? / Davenport, James.

In: CEUR Workshop Proceedings, Vol. 1889, 2017.

Research output: Contribution to journalArticle

@article{b6248589fe164ca0b56b41c212b549c2,
title = "SMT Nonlinear Real Arithmetic and Computer Algebra: A dialogue of the deaf?",
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.",
author = "James Davenport",
year = "2017",
language = "English",
volume = "1889",
journal = "CEUR Workshop Proceedings",
issn = "1613-0073",
publisher = "CEUR-WS",

}

TY - JOUR

T1 - SMT Nonlinear Real Arithmetic and Computer Algebra

T2 - A dialogue of the deaf?

AU - Davenport, James

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85030107139&partnerID=8YFLogxK

M3 - Article

VL - 1889

JO - CEUR Workshop Proceedings

JF - CEUR Workshop Proceedings

SN - 1613-0073

ER -