Real quantifier elimination by computation of comprehensive Gröbner systems

Ryoya Fukasaku; Hidenao Iwane; Yosuke Sato

doi:10.1145/2755996.2756646

Real quantifier elimination by computation of comprehensive Gröbner systems

Ryoya Fukasaku, Hidenao Iwane, Yosuke Sato

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

14 Citations (Scopus)

Abstract

A real quantifier elimination method based on the theory of real root counting and the computation of comprehensive Gröbner systems introduced by V. Weispfenning is studied in more detail. We introduce a simpler and more intuitive algorithm which is shown to be an improvement of the original algorithm. Our algorithm is implemented on the computer algebra system Maple using a recent algorithm to compute comprehensive Gröbner systems together with several simplification techniques. According to our computation experiments, our program is superior to other existing implementations for many examples which contain many equalities.

Original language	English
Title of host publication	ISSAC 2015 - Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation
Publisher	Association for Computing Machinery
Pages	173-180
Number of pages	8
ISBN (Electronic)	9781450334358
DOIs	https://doi.org/10.1145/2755996.2756646
Publication status	Published - Jun 24 2015
Externally published	Yes
Event	40th ACM International Symposium on Symbolic and Algebraic Computation, ISSAC 2015 - Bath, United Kingdom Duration: Jul 6 2015 → Jul 9 2015

Publication series

Name	Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC
Volume	2015-June

Conference

Conference	40th ACM International Symposium on Symbolic and Algebraic Computation, ISSAC 2015
Country/Territory	United Kingdom
City	Bath
Period	7/6/15 → 7/9/15

All Science Journal Classification (ASJC) codes

Mathematics(all)

Access to Document

10.1145/2755996.2756646

Cite this

Fukasaku, R., Iwane, H., & Sato, Y. (2015). Real quantifier elimination by computation of comprehensive Gröbner systems. In ISSAC 2015 - Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation (pp. 173-180). (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC; Vol. 2015-June). Association for Computing Machinery. https://doi.org/10.1145/2755996.2756646

Real quantifier elimination by computation of comprehensive Gröbner systems. / Fukasaku, Ryoya; Iwane, Hidenao; Sato, Yosuke.
ISSAC 2015 - Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation. Association for Computing Machinery, 2015. p. 173-180 (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC; Vol. 2015-June).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Fukasaku, R, Iwane, H & Sato, Y 2015, Real quantifier elimination by computation of comprehensive Gröbner systems. in ISSAC 2015 - Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation. Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC, vol. 2015-June, Association for Computing Machinery, pp. 173-180, 40th ACM International Symposium on Symbolic and Algebraic Computation, ISSAC 2015, Bath, United Kingdom, 7/6/15. https://doi.org/10.1145/2755996.2756646

Fukasaku R, Iwane H, Sato Y. Real quantifier elimination by computation of comprehensive Gröbner systems. In ISSAC 2015 - Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation. Association for Computing Machinery. 2015. p. 173-180. (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC). doi: 10.1145/2755996.2756646

Fukasaku, Ryoya ; Iwane, Hidenao ; Sato, Yosuke. / Real quantifier elimination by computation of comprehensive Gröbner systems. ISSAC 2015 - Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation. Association for Computing Machinery, 2015. pp. 173-180 (Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC).

@inproceedings{9428802f92204465bb81557d4f10c7ba,

title = "Real quantifier elimination by computation of comprehensive Gr{\"o}bner systems",

abstract = "A real quantifier elimination method based on the theory of real root counting and the computation of comprehensive Gr{\"o}bner systems introduced by V. Weispfenning is studied in more detail. We introduce a simpler and more intuitive algorithm which is shown to be an improvement of the original algorithm. Our algorithm is implemented on the computer algebra system Maple using a recent algorithm to compute comprehensive Gr{\"o}bner systems together with several simplification techniques. According to our computation experiments, our program is superior to other existing implementations for many examples which contain many equalities.",

author = "Ryoya Fukasaku and Hidenao Iwane and Yosuke Sato",

year = "2015",

month = jun,

day = "24",

doi = "10.1145/2755996.2756646",

language = "English",

series = "Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC",

publisher = "Association for Computing Machinery",

pages = "173--180",

booktitle = "ISSAC 2015 - Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation",

}

TY - GEN

T1 - Real quantifier elimination by computation of comprehensive Gröbner systems

AU - Fukasaku, Ryoya

AU - Iwane, Hidenao

AU - Sato, Yosuke

PY - 2015/6/24

Y1 - 2015/6/24

N2 - A real quantifier elimination method based on the theory of real root counting and the computation of comprehensive Gröbner systems introduced by V. Weispfenning is studied in more detail. We introduce a simpler and more intuitive algorithm which is shown to be an improvement of the original algorithm. Our algorithm is implemented on the computer algebra system Maple using a recent algorithm to compute comprehensive Gröbner systems together with several simplification techniques. According to our computation experiments, our program is superior to other existing implementations for many examples which contain many equalities.

AB - A real quantifier elimination method based on the theory of real root counting and the computation of comprehensive Gröbner systems introduced by V. Weispfenning is studied in more detail. We introduce a simpler and more intuitive algorithm which is shown to be an improvement of the original algorithm. Our algorithm is implemented on the computer algebra system Maple using a recent algorithm to compute comprehensive Gröbner systems together with several simplification techniques. According to our computation experiments, our program is superior to other existing implementations for many examples which contain many equalities.

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

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

U2 - 10.1145/2755996.2756646

DO - 10.1145/2755996.2756646

M3 - Conference contribution

AN - SCOPUS:84957631885

T3 - Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC

SP - 173

EP - 180

BT - ISSAC 2015 - Proceedings of the 2015 ACM International Symposium on Symbolic and Algebraic Computation

PB - Association for Computing Machinery

T2 - 40th ACM International Symposium on Symbolic and Algebraic Computation, ISSAC 2015

Y2 - 6 July 2015 through 9 July 2015

ER -

Real quantifier elimination by computation of comprehensive Gröbner systems

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this