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 proceedingpeer-review

    2 Citations (Scopus)
    25 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
    Country/TerritoryAustria
    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