An SMT solver for non-linear real arithmetic inside maple

Research output: Contribution to journalArticlepeer-review

69 Downloads (Pure)


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


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


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

Cite this