On the Efficiency of Geometry Theorem Proving by Grobner Bases

DOI Web Site 13 References
  • Moritsugu Shuichi
    University of Tsukuba Graduate School of Library, Information and Media Studies
  • Arai Chisato
    University of Tsukuba Graduate School of Library, Information and Media Studies

Bibliographic Information

Other Title
  • グレブナー基底による幾何定理の代数的証明の効率について
  • グレブナー キテイ ニ ヨル キカ テイリ ノ ダイスウテキ ショウメイ ノ コウリツ ニ ツイテ

Search this article

Description

We show experimental results for proving Euclidean geometry theorems by Grobner bases method. In 1988, Chou Shang-Ching proved 512 theorems by Wu's method, and reported that 35 of them remained unsolvable by Grobner bases method. In this paper, we tried to prove these 35 theorems by Grobner basis method using three kinds of computer algebra systems : Reduce, Maple and Risa/Asir. As a result, we succeeded in proving 26 theorems but have found that the rest 9 theorems are essentially difficult to compute Grobner vases. We show the table of timing data and discuss several devices to complete the proof.

Journal

References(13)*help

See more

Details 詳細情報について

Report a problem

Back to top