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

James H. Davenport; Matthew England

doi:10.1007/978-3-319-72453-9_22

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

Coventry University

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

2 Citations (SciVal)

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 ² 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 language	English
Title of host publication	Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Proceedings
Place of Publication	Germany
Publisher	Springer Verlag
Pages	280-285
Number of pages	6
ISBN (Print)	9783319724522
DOIs	https://doi.org/10.1007/978-3-319-72453-9_22
Publication status	Published - 2017
Event	7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017 - Vienna, Austria Duration: 15 Nov 2017 → 17 Nov 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10693

Conference

Conference	7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017
Country/Territory	Austria
City	Vienna
Period	15/11/17 → 17/11/17

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

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 ). 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 or section in a book/report/conference proceeding › Chapter in a published conference proceeding

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)). doi: 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",

note = "7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017 ; Conference date: 15-11-2017 Through 17-11-2017",

}

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 - Chapter in a published conference proceeding

AN - SCOPUS:85039413521

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

T2 - 7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017

Y2 - 15 November 2017 through 17 November 2017

ER -

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

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

SC-square - Satisfiability Checking and Symbolic Computation: uniting two communities to solve real problems

Real Geometry and Connectedness via Triangular Description

Cite this

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

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

SC-square - Satisfiability Checking and Symbolic Computation: uniting two communities to solve real problems

Real Geometry and Connectedness via Triangular Description

Cite this