swMATH ID: 20574
Software Authors: Fukasaku, Ryoya; Iwane, Hidenao; Sato, Yosuke
Description: CGSQE/SyNRAC: a real quantifier elimination package based on the computation of comprehensive Gr”obner systems. 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”obner 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.
Homepage: http://dl.acm.org/citation.cfm?id=3015313
Dependencies: Maple
Related Software: REDLOG; QEPCAD; PGB; SYNRAC; Maple
Cited in: 2 Publications

Citations by Year