nach oben

Journal of Automated Reasoning

Erschienen in:

22.11.2016

Automated Reducible Geometric Theorem Proving and Discovery by Gröbner Basis Method

verfasst von: Jie Zhou, Dingkang Wang, Yao Sun

Erschienen in: Journal of Automated Reasoning | Ausgabe 3/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

In this paper, we investigate the problem that the conclusion is true on some components of the hypotheses for a geometric statement. In that case, the affine variety associated with the hypotheses is reducible. A polynomial vanishes on some but not all the components of a variety if and only if it is a zero divisor in a quotient ring with respect to the radical ideal defined by the variety. Based on this fact, we present an algorithm to decide if a geometric statement is generally true or generally true on components by the Gröbner basis method. This method can also be used in geometric theorem discovery, which can give the complementary conditions such that the geometric statement becomes true or true on components. Some reducible geometric statements are given to illustrate our method.

Vorheriger Artikel A Semantic Framework for Proof Evidence

Nächster Artikel Markov Chains and Markov Decision Processes in Isabelle/HOL

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Programs for computing minimal comprehensive Gröbner systems, which is based on the algorithm in [23], are available at http://mmrc.iss.ac.cn/~dwang/software.html.

The variables are divided in three blocks y, X, and U. A monomial ordering is chosen for each block. To compare two monomials, we firstly compare their y part. If the y part is equal, then we compare their X part. If the y and X parts are equal, then we compare their U part.

Gelernter, H., Hanson, J.R., Loveland, D.W.: Empirical explorations of the geometry-theorem proving machine. In: Proceeding of the West Joint Computer Conference, pp. 143–147 (1960)

Tarski, A.: A decision method for elementary algebra and geometry. Texts Monogr. Symb. Comput. 35, 24–84 (1951)MathSciNetMATH

Seidenberg, A.: A new decision method for elememtary algebra. Ann. Math. 60(2), 365–374 (1954)MathSciNetCrossRefMATH

Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 85–121. Springer, Vienna (1998)

Wu, W.T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Sci. Sin. 21, 159–172 (1978)MathSciNetMATH

Wu, W.T.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2(3), 221–252 (1986)CrossRefMATH

Chou, S.C.: Mechanical Geometry Theorem Proving, Mathematics and Its Applications. Reidel, Amsterdam (1988)

Ritt, J.F.: Differential equations from the algebraic standpoint. Am. Math. Soc. (1932)

Chou, S.C.: Proving geometry theorems with rewrite rules. J. Autom. Reason. 2(3), 253–273 (1986)CrossRefMATH

10.

Kapur, D.: Geometry theorem proving using Hilbert’s Nullstellensatz. In: Proceedings of the ISSAC, pp. 202–208. ACM Press, New York (1986)

11.

Kutzler, B., Stifter, S.: Automated geometry theorem proving using Buchberger’s algorithm. In: Proceedings of ISSAC, pp. 209–214. ACM Press, New York (1986)

12.

Coxeter, H.S.M.: Introduction to Geometry. Wiley, New York (1961)MATH

13.

Taylor, K.B.: Three circles with collinear centers. Am. Math. Mon. 90, 484–486 (1983)

14.

Dalzotto, G., Recio, T.: On protocols for the automated discovery of theorems in elementary geometry. J. Autom. Reason. 43(2), 203–236 (2009)MathSciNetCrossRefMATH

15.

Botana, F., Montes, A., Recio, T.: An algorithm for automatic discovery of algebraic loci. In: Proceedings of the ADG, pp. 53–59 (2012)

16.

Chen, X.F., Li, P., Lin, L., Wang, D.K.: Proving geometric theorems by partitioned-parametric Gröbner bases. In: Proceedings of the ADG, pp. 34–43 (2004)

17.

Montes, A., Recio, T.: Automatic discovery of geometry theorems using minimal canonical comprehensive Gröbner systems. In: Proceedings of the ADG, pp. 113–138 (2006)

18.

Recio, T., Velez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23(1), 63–82 (1999)MathSciNetCrossRefMATH

19.

Wang, D.K., Lin, L.: Automatic discovery of geometric theorem by computing Gröbner bases with parameters. In: Abstracts of Presentations of ACA, vol. 32, Japan (2005)

20.

Winkler, F.: Gröbner bases in geometry theorem proving and simplest degeneracy conditions. Math. Pannon. 1(1), 15–32 (1990)MathSciNetMATH

21.

Weispfenning, V.: Comprehensive Gröbner bases. J. Symb. Comput. 14(1), 1–29 (1992)MathSciNetCrossRefMATH

22.

Kapur, D.: An approach for solving systems of parametric polynomial equations. In: Saraswat, V., Van Hentenryck, (eds.) Principles and Practices of Constraints Programming, pp. 217–244. MIT Press, Cambridge (1995)

23.

Kapur, D., Sun, Y., Wang, D.K.: A new algorithm for computing comprehensive Gröbner systems. In: Proceedings of the ISSAC, pp. 29–36. ACM Press, New York (2010)

24.

Montes, A.: A new algorithm for discussing Gröbner bases with parameters. J. Symb. Comput. 33(2), 183–208 (2002)CrossRefMATH

25.

Montes, A., Wibmer, M.: Gröbner bases for polynomial systems with parameters. J. Symb. Comput. 45(12), 1391–1425 (2010)CrossRefMATH

26.

Nabeshima, K.: A speed-up of the algorithm for computing comprehensive Gröbner systems. In: Proceedings of the ISSAC, pp. 299–306. ACM Press, New York (2007)

27.

Suzuki, A., Sato, Y.: An alternative approach to comprehensive Gröbner bases. J. Symb. Comput. 36(3), 649–667 (2003)CrossRefMATH

28.

Weispfenning, V.: Canonical comprehensive Gröbner bases. J. Symb. Comput. 36(3), 669–683 (2003)MathSciNetCrossRefMATH

29.

Manubens, M., Montes, A.: Minimal canonical comprehensive Groebner system. J. Symb. Comput. 44(5), 463–478 (2009)CrossRefMATH

30.

Cox, D., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms, 3rd edn. Springer, New York (2007)CrossRefMATH

Titel: Automated Reducible Geometric Theorem Proving and Discovery by Gröbner Basis Method
verfasst von: Jie Zhou
Dingkang Wang
Yao Sun
Publikationsdatum: 22.11.2016
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 3/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-016-9395-z

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner