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 contribution

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 2 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 - 7th International Conference, MACIS 2017, Proceedings
Place of PublicationGermany
PublisherSpringer Verlag
Pages280-285
Number of pages6
ISBN (Print)9783319724522
DOIs
Publication statusPublished - 2017
Event7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017 - Vienna, Austria
Duration: 15 Nov 201717 Nov 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10693

Conference

Conference7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
CountryAustria
CityVienna
Period15/11/1717/11/17

Fingerprint

Modulo
Decomposition
Decompose
Quantifier Elimination
Polynomial Systems
Symbolic Computation
Decision Procedures
Polynomials
Restriction

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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 - 7th International Conference, MACIS 2017, Proceedings (pp. 280-285). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10693 ). Germany: Springer Verlag. https://doi.org/10.1007/978-3-319-72453-9_22

The potential and challenges of CAD with equational constraints for SC-square. / Davenport, James H.; England, Matthew.

Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings. Germany : Springer Verlag, 2017. p. 280-285 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10693 ).

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

Davenport, JH & England, M 2017, The potential and challenges of CAD with equational constraints for SC-square. in Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10693 , Springer Verlag, Germany, pp. 280-285, 7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017, Vienna, Austria, 15/11/17. https://doi.org/10.1007/978-3-319-72453-9_22
Davenport JH, England M. The potential and challenges of CAD with equational constraints for SC-square. In Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings. Germany: Springer Verlag. 2017. p. 280-285. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-72453-9_22
Davenport, James H. ; England, Matthew. / The potential and challenges of CAD with equational constraints for SC-square. Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings. Germany : Springer Verlag, 2017. pp. 280-285 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a63a24a38d194570a1f9dfbba1e3f18e,
title = "The potential and challenges of CAD with equational constraints for SC-square",
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 2 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.",
author = "Davenport, {James H.} and Matthew England",
year = "2017",
doi = "10.1007/978-3-319-72453-9_22",
language = "English",
isbn = "9783319724522",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "280--285",
booktitle = "Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings",
address = "Germany",

}

TY - GEN

T1 - The potential and challenges of CAD with equational constraints for SC-square

AU - Davenport, James H.

AU - England, Matthew

PY - 2017

Y1 - 2017

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

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

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

U2 - 10.1007/978-3-319-72453-9_22

DO - 10.1007/978-3-319-72453-9_22

M3 - Conference contribution

SN - 9783319724522

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 280

EP - 285

BT - Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings

PB - Springer Verlag

CY - Germany

ER -