The Potential and Challenges of CAD with Equational Constraints for SC-Square

James H. Davenport, Matthew England

Research output: Chapter in Book/Report/Conference proceedingConference proceeding

4 Downloads (Pure)

Abstract

Cylindrical algebraic decomposition (CAD) is a core algorithm within Symbolic Computation, particularly for quantifier elimination over the reals and polynomial systems solving more generally. It is now finding increased application as a decision procedure for Satisfiability Modulo Theories (SMT) solvers when working with non-linear real arithmetic. We discuss the potentials from increased focus on the logical structure of the input brought by the SMT applications and SC-Square project, particularly the presence of equational constraints. We also highlight the challenges for exploiting these: primitivity restrictions, well-orientedness questions, and the prospect of incrementality.
Original languageEnglish
Title of host publicationMathematical Aspects of Computer and Information Sciences (Proc. MACIS '17)
Subtitle of host publicationMACIS 2017
PublisherSpringer
Pages280-285
Number of pages6
VolumeLNCS 10693
ISBN (Electronic)978-3-319-72453-9
ISBN (Print)978-3-319-72452-2
DOIs
Publication statusPublished - 21 Dec 2017
Event7th International Conference on Mathematical Aspects of Computer and Information Sciences - Vienna, Austria
Duration: 15 Nov 201717 Nov 2017
Conference number: 7
https://macis2017.sba-research.org/

Publication series

NameLecture Notes in Computer Science (LNCS)
PublisherSpringer

Conference

Conference7th International Conference on Mathematical Aspects of Computer and Information Sciences
Abbreviated titleMACIS 2017
CountryAustria
CityVienna
Period15/11/1717/11/17
Internet address

Bibliographical note

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-72453-9_22

Fingerprint Dive into the research topics of 'The Potential and Challenges of CAD with Equational Constraints for SC-Square'. Together they form a unique fingerprint.

  • Cite this

    Davenport, J. H., & England, M. (2017). The Potential and Challenges of CAD with Equational Constraints for SC-Square. In Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17): MACIS 2017 (Vol. LNCS 10693, pp. 280-285). (Lecture Notes in Computer Science (LNCS)). Springer. https://doi.org/10.1007/978-3-319-72453-9_22