CGSQE/SyNRAC - A real quantifier elimination package based on the computation of comprehensive Gröbner systems

Ryoya Fukasaku, Hidenao Iwane, Yosuke Sato

Research output: Contribution to journalArticle

1 Citation (Scopus)


CGSQE is a Maple package for real quantifier elimination (QE) we are developing. It works cooperating with SyNRAC which is also a Maple package for real QE one of the authors is developing. For a given first order formula, CGSQE eliminates all possible quantifiers using the underlying equational constraints by the computation of comprehensive Gröbner systems (CGSs). In case all quantifiers are not removable, it transforms the given formula into a formula which contains only strict inequalities of quantified variables, then uses a cylindrical algebraic decomposition based real QE program of SyNRAC to remove the remaining quantifiers. The core algorithm of CGSQE is a CGS real QE algorithm which was first introduced by Weispfenning in 1998 and further improved by us in 2015 so that we can make a satisfactorily practical implementation. CGSQE is superior to other real QE implementations for many examples which contain many equational constraints. In the software presentation, we would like to show high-performance computation of CGSQE.

Original languageEnglish
Article number3015313
Pages (from-to)101-104
Number of pages4
JournalACM Communications in Computer Algebra
Issue number3
Publication statusPublished - Sep 2016
Externally publishedYes


All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Computational Mathematics

Cite this