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

Ryoya Fukasaku, Hidenao Iwane, Yosuke Sato

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

1 引用 (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.

元の言語英語
記事番号3015313
ページ(範囲)101-104
ページ数4
ジャーナルACM Communications in Computer Algebra
50
発行部数3
DOI
出版物ステータス出版済み - 9 1 2016
外部発表Yes

Fingerprint

Quantifier Elimination
Quantifiers
Maple
Decomposition
Eliminate
High Performance
Transform
First-order
Decompose
Software

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Computational Mathematics

これを引用

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, 01.09.2016, p. 101-104.

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

@article{f904ceffe8044024a407b460ab257096,
title = "CGSQE/SyNRAC - A real quantifier elimination package based on the computation of comprehensive Gr{\"o}bner systems",
abstract = "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{\"o}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.",
author = "Ryoya Fukasaku and Hidenao Iwane and Yosuke Sato",
year = "2016",
month = "9",
day = "1",
doi = "10.1145/3015306.3015313",
language = "English",
volume = "50",
pages = "101--104",
journal = "ACM Communications in Computer Algebra",
issn = "1932-2232",
publisher = "Association for Computing Machinery (ACM)",
number = "3",

}

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 -