An SMT solver for non-linear real arithmetic inside maple

Research output: Contribution to journalArticlepeer-review

69 Downloads (Pure)

Abstract

We report on work-in-progress to create an SMT-solver inside Maple for non-linear real arithmetic (NRA). We give background information on the algorithm being implemented: cylindrical algebraic coverings as a theory solver in the lazy SMT paradigm. We then present some new work on the identification of minimal conflicting cores from the coverings.
Original languageEnglish
Pages (from-to)76-79
Number of pages4
JournalACM Communications in Computer Algebra
Volume56
Issue number2
DOIs
Publication statusPublished - 23 Nov 2022

Bibliographical note

© ACM, 2022. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Communications in Computer Algebra, vol. 56, no. 2, pp. 76-79.http://doi.acm.org/10.1145/3572867.3572880

Keywords

  • Computer Algebra
  • Symbolic computation
  • satisfiability modulo theories
  • cylindrical algebraic coverings
  • Set covering problem

Fingerprint

Dive into the research topics of 'An SMT solver for non-linear real arithmetic inside maple'. Together they form a unique fingerprint.

Cite this