### 抄録

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.

元の言語 | 英語 |
---|---|

記事番号 | 3015313 |

ページ（範囲） | 101-104 |

ページ数 | 4 |

ジャーナル | ACM Communications in Computer Algebra |

巻 | 50 |

発行部数 | 3 |

DOI | |

出版物ステータス | 出版済み - 9 1 2016 |

外部発表 | Yes |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Computational Theory and Mathematics
- Computational Mathematics

### これを引用

*ACM Communications in Computer Algebra*,

*50*(3), 101-104. [3015313]. https://doi.org/10.1145/3015306.3015313

**CGSQE/SyNRAC - A real quantifier elimination package based on the computation of comprehensive Gröbner systems.** / Fukasaku, Ryoya; Iwane, Hidenao; Sato, Yosuke.

研究成果: ジャーナルへの寄稿 › 記事

*ACM Communications in Computer Algebra*, 巻. 50, 番号 3, 3015313, pp. 101-104. https://doi.org/10.1145/3015306.3015313

}

TY - JOUR

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

AU - Fukasaku, Ryoya

AU - Iwane, Hidenao

AU - Sato, Yosuke

PY - 2016/9/1

Y1 - 2016/9/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84994890250&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84994890250&partnerID=8YFLogxK

U2 - 10.1145/3015306.3015313

DO - 10.1145/3015306.3015313

M3 - Article

VL - 50

SP - 101

EP - 104

JO - ACM Communications in Computer Algebra

JF - ACM Communications in Computer Algebra

SN - 1932-2232

IS - 3

M1 - 3015313

ER -