Making a quantifier elimination method based on the theory of comprehensive Groebner systems more efficient

• Project/Area Number: 17K12642
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: Kyushu University (2019-2020); Tokyo University of Science (2017-2018)
• Principal Investigator: Fukasaku Ryoya 九州大学, 数理学研究院, 助教 (40778924)
• Project Period (FY): 2017-04-01 – 2021-03-31
• Project Status: Completed (Fiscal Year 2020)
• Budget Amount: ¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000); Fiscal Year 2019: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2018: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
• Keywords: 限量子消去 / 包括的グレブナー基底系 / パラメータ付き多項式イデアル / 計算機代数 / 数式処理 / ホップ分岐 / 計算代数 / 包括的グレブナー基底 / グレブナー基底 / 限量子消去法 / 効率化 / 飽和イデアル / 数式処理システム / 実閉体 / エルミート二次形式 / アルゴリズム

Outline of Final Research Achievements

We can compute formulas without quantified variables which is equivalent to given first order formulas by using quantifier elimination methods. In order to make quantifier elimination for first order formulas containg many equalities more efficient, we have tried to make a quantifier elimination method based on the theory of comprehensive Groebner systems more efficient. We proposed a method for efficiently computing parametric zero-dimensional saturation ideals, and a method for computing Hermitian quadratic forms of parametric zero-dimensional radical ideals without computing such ideals.

Academic Significance and Societal Importance of the Research Achievements

一階述語論理式の記述能力は高く、数学だけでなく物理・工学などで発生する多くの数理問題や数理モデルを正確に表現できる。そうした一階述語論理式から、限量子を消去した、等価な論理式を計算する限量子消去法は、数理問題や数理モデルに対する正確かつ簡略化された表現を与え、問題やモデルの本質を明らかにする。等式制約は不等式制約に比べて強い制約を持っていることから数理問題や数理モデルの本質となっている場合も多いため、等式制約の多い一階述語論理式に対する効率化は重要である。

Research Products

• [Journal Article] On parametric border bases (2020)
  • Author(s): Yosuke Sato, Hiroshi Sekigawa, Ryoya Fukasaku, Katsusuke Nabeshima
  • Journal Title: Lecture Notes in Computer Science Volume: 11989 Pages: 10-15
  • DOI: 10.1007/978-3-030-43120-4_2
  • ISBN: 9783030431198, 9783030431204
  • Peer Reviewed
• [Journal Article] On Multivariate Hermitian Quadratic Forms (2019)
  • Author(s): Ryoya Fukasaku, Hidenao Iwane, Yosuke Sato
  • Journal Title: Mathematics in Computer Science Volume: 13 Issue: 1-2 Pages: 79-93
  • DOI: 10.1007/s11786-018-0387-8
  • Peer Reviewed / Open Access
• [Journal Article] On Continuity of the Roots of a Parametric Zero Dimensional Multivariate Polynomial Ideal (2018)
  • Author(s): Sato Yosuke、Fukasaku Ryoya、Sekigawa Hiroshi
  • Journal Title: Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation Volume: 2018 Pages: 359-365
  • DOI: 10.1145/3208976.3209004
  • Peer Reviewed / Open Access
• [Journal Article] On Multivariate Hermitian Quadratic Forms (2018)
  • Author(s): Ryoya Fukasaku, Hidenao Iwane and Yosuke Sato
  • Journal Title: Mathematics in Computer Science Volume: 印刷中
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] Can an A.I. win a medal in the mathematical olympiad? Benchmarking mechanized mathematics on pre-university problems (2018)
  • Author(s): Takuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhand, Ryoya Fukasaku, Jumma Kudo, Hirokazu Anai, and Noriko H. Arai
  • Journal Title: AI Communications Volume: 印刷中
  • NAID: 120006517663
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] On continuity of the roots of a parametric zero dimensional multivariate polynomial ideal (2018)
  • Author(s): Yosuke Sato, Ryoya Fukasaku and Hiroshi Sekigawa
  • Journal Title: Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC) 2018 Volume: 印刷中
  • Peer Reviewed / Int'l Joint Research
• [Journal Article] On Multivariate Hermitian Quadratic Forms (2017)
  • Author(s): Ryoya Fukasaku and Hidenao Iwane
  • Journal Title: Book of Abstracts, 23rd Conference on Applications of Computer Algebra Volume: - Pages: 222-223
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] On Real Roots Counting for Non-radical Parametric Ideals (2017)
  • Author(s): Fukasaku Ryoya、Sato Yosuke
  • Journal Title: Proceedings of Mathematical Aspects of Computer and Information Sciences - 7th International Conference, MACIS 2017, Lecture Notes in Computer Science Volume: 10693 Pages: 258-263
  • DOI: 10.1007/978-3-319-72453-9_18
  • ISBN: 9783319724522, 9783319724539
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Journal Article] 包括的グレブナー基底系を利用した限量子消去における包括的グレブナー基底系計算 (2017)
  • Author(s): 深作 亮也,岩根 秀直,佐藤 洋祐
  • Journal Title: 数式処理 Volume: 23 (2) Pages: 116-119
  • Open Access
• [Journal Article] 不等式制約をもつ論理式に対する包括的グレブナー基底系を利用した限量記号消去の出力の簡単化 (2017)
  • Author(s): 岩根 秀直,深作 亮也,佐藤 洋祐
  • Journal Title: 数式処理 Volume: 23 (2) Pages: 120-123
  • Open Access
• [Journal Article] 不等式制約をもつ論理式に対する包括的グレブナー基底系を利用した限量記号消去の出力の簡単化 (2017)
  • Author(s): 岩根 秀直,深作 亮也,佐藤 洋祐
  • Journal Title: 数理解析研究所講究録 Volume: 2019 Pages: 124-142
  • Open Access
• [Journal Article] 飽和イデアル計算なしのCGS-QE (2017)
  • Author(s): 深作 亮也,岩根 秀直,佐藤 洋祐
  • Journal Title: 数理解析研究所講究録 Volume: 2019 Pages: 113-123
  • Open Access
• [Journal Article] On Possible Use of Quantifier Elimination Software in Upper Secondary Mathematics Education (2017)
  • Author(s): Yosuke Sato and Ryoya Fukasaku
  • Journal Title: Proceedings of the 22nd Asian Technology Conference in Mathematics Volume: -
  • Peer Reviewed / Open Access / Int'l Joint Research
• [Presentation] 重複ホップ分岐が発生するようなパラメータ条件の計算アルゴリズム (2020)
  • Author(s): 深作亮也
  • Organizer: 日本数式処理学会第29回大会
• [Presentation] 単純ホップ分岐判定法の実装 (2020)
  • Author(s): 深作亮也,田島慎一
  • Organizer: RIMS共同研究(公開型)Computer Algebra Theory and its Applications
• [Presentation] On Parametric Border Bases (2019)
  • Author(s): Yosuke Sato, Hiroshi Sekigawa, Ryoya Fukasaku, Katsusuke Nabeshima
  • Organizer: Mathematical Aspects of Computer and Information Sciences - 8th International Conference, MACIS 2019
  • Int'l Joint Research
• [Presentation] On Continuity of the Roots of a Parametric Zero Dimensional Multivariate Polynomial Ideal (2018)
  • Author(s): Ryoya Fukasaku
  • Organizer: International Symposium on Symbolic and Algebraic Computation
  • Int'l Joint Research
• [Presentation] 実限量子消去とその応用について (2018)
  • Author(s): 深作亮也
  • Organizer: 応用特異点論研究集会
  • Invited
• [Presentation] On continuity of the roots of a parametric zero dimensional multivariate polynomial ideal (2018)
  • Author(s): Yosuke Sato, Ryoya Fukasaku and Hiroshi Sekigawa
  • Organizer: the International Symposium on Symbolic and Algebraic Computation (ISSAC) 2018
  • Int'l Joint Research
• [Presentation] 根基イデアルに対するエルミート二次形式について (2017)
  • Author(s): 深作亮也
  • Organizer: 日本数式処理学会第26回大会
• [Presentation] On multivariate Hermitian quadratic forms (2017)
  • Author(s): Ryoya Fukasaku and Hidenao Iwane
  • Organizer: 23rd Conference on Applications of Computer Algebra
  • Int'l Joint Research
• [Presentation] CGBとCGSの入門 (2017)
  • Author(s): 深作亮也
  • Organizer: 平成29 年度ＲＩＭＳ共同研究（グループ型） 数式処理の新たな発展－その最新研究と他分野との連携－
  • Invited
• [Presentation] パラメータ付き非根基イデアルに対するエルミート二次形式について (2017)
  • Author(s): 深作亮也
  • Organizer: 平成29 年度ＲＩＭＳ共同研究（グループ型） 数式処理の新たな発展－その最新研究と他分野との連携－
• [Presentation] On Real Roots Counting for Non-radical Parametric Ideals (2017)
  • Author(s): Ryoya Fukasaku and Yosuke Sato
  • Organizer: 7th International Conference on Mathematical Aspects of Computer and Information Sciences
  • Int'l Joint Research
• [Presentation] On Possible Use of Quantifier Elimination Software in Upper Secondary Mathematics Education (2017)
  • Author(s): Yosuke Sato and Ryoya Fukasaku
  • Organizer: the 22nd Asian Technology Conference in Mathematics
  • Int'l Joint Research
• [Remarks] 限量子消去プログラムCGSQE公開ページ
  • URL: http://www.rs.tus.ac.jp/fukasaku/software/CGSQE-2018/