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

James H. Davenport, Matthew England

University of Bath

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

1 Citation (Scopus)

18 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 language	English
Title of host publication	Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17)
Subtitle of host publication	MACIS 2017
Publisher	Springer
Pages	280-285
Number of pages	6
Volume	LNCS 10693
ISBN (Electronic)	978-3-319-72453-9
ISBN (Print)	978-3-319-72452-2
DOIs	https://doi.org/10.1007/978-3-319-72453-9_22
Publication status	Published - 21 Dec 2017
Event	7th International Conference on Mathematical Aspects of Computer and Information Sciences - Vienna, Austria Duration: 15 Nov 2017 → 17 Nov 2017 Conference number: 7 https://macis2017.sba-research.org/

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Publisher	Springer

Conference

Conference	7th International Conference on Mathematical Aspects of Computer and Information Sciences
Abbreviated title	MACIS 2017
Country/Territory	Austria
City	Vienna
Period	15/11/17 → 17/11/17
Internet address	https://macis2017.sba-research.org/

Bibliographical note

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

Access to Document

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

Post-PrintAccepted author manuscript, 710 KBLicence: CC BY

Cite this

The Potential and Challenges of CAD with Equational Constraints for SC-Square. / Davenport, James H.; England, Matthew.

Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17): MACIS 2017. Vol. LNCS 10693 Springer, 2017. p. 280-285 (Lecture Notes in Computer Science (LNCS)).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

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 (Proc. MACIS '17): MACIS 2017. vol. LNCS 10693, Lecture Notes in Computer Science (LNCS), Springer, pp. 280-285, 7th International Conference on Mathematical Aspects of Computer and Information Sciences, Vienna, Austria, 15/11/17. https://doi.org/10.1007/978-3-319-72453-9_22

@inproceedings{9a6157d23b8a468194cd67d08bdef0e6,

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-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.",

author = "Davenport, {James H.} and Matthew England",

note = "The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-72453-9_22; 7th International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2017 ; Conference date: 15-11-2017 Through 17-11-2017",

year = "2017",

month = dec,

day = "21",

doi = "10.1007/978-3-319-72453-9_22",

language = "English",

isbn = "978-3-319-72452-2",

volume = "LNCS 10693",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "280--285",

booktitle = "Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17)",

address = "United Kingdom",

url = "https://macis2017.sba-research.org/",

}

TY - GEN

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

AU - Davenport, James H.

AU - England, Matthew

N1 - Conference code: 7

PY - 2017/12/21

Y1 - 2017/12/21

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

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

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

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

M3 - Conference proceeding

SN - 978-3-319-72452-2

VL - LNCS 10693

T3 - Lecture Notes in Computer Science (LNCS)

SP - 280

EP - 285

BT - Mathematical Aspects of Computer and Information Sciences (Proc. MACIS '17)

PB - Springer

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

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

Bibliographical note

Access to Document

Fingerprint

Cite this