<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>SMT Nonlinear Real Arithmetic and Computer Algebra: a Dialogue of the Deaf ?</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>James Davenport</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>University of Bath</institution>
        </aff>
      </contrib-group>
      <abstract>
        <p>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.</p>
      </abstract>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list />
  </back>
</article>