×

Automated reducible geometric theorem proving and discovery by Gröbner basis method. (English) Zbl 1425.68383

Summary: 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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases)
51M04 Elementary problems in Euclidean geometries

Software:

PGB
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] 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) · Zbl 1184.68458
[2] Tarski, A.: A decision method for elementary algebra and geometry. Texts Monogr. Symb. Comput. 35, 24-84 (1951) · Zbl 0900.03045
[3] Seidenberg, A.: A new decision method for elememtary algebra. Ann. Math. 60(2), 365-374 (1954) · Zbl 0056.01804 · doi:10.2307/1969640
[4] 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) · Zbl 0900.03055
[5] Wu, W.T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Sci. Sin. 21, 159-172 (1978) · Zbl 0376.68057
[6] Wu, W.T.: Basic principles of mechanical theorem proving in elementary geometries. J. Autom. Reason. 2(3), 221-252 (1986) · Zbl 0642.68163 · doi:10.1007/BF02328447
[7] Chou, S.C.: Mechanical Geometry Theorem Proving, Mathematics and Its Applications. Reidel, Amsterdam (1988)
[8] Ritt, J.F.: Differential equations from the algebraic standpoint. Am. Math. Soc. (1932) · JFM 58.0445.06
[9] Chou, S.C.: Proving geometry theorems with rewrite rules. J. Autom. Reason. 2(3), 253-273 (1986) · Zbl 0642.68162 · doi:10.1007/BF02328448
[10] Kapur, D.: Geometry theorem proving using Hilbert’s Nullstellensatz. In: Proceedings of the ISSAC, pp. 202-208. ACM Press, New York (1986) · Zbl 0376.68057
[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) · Zbl 0629.68086
[12] Coxeter, H.S.M.: Introduction to Geometry. Wiley, New York (1961) · Zbl 0095.34502
[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) · Zbl 1184.68458 · doi:10.1007/s10817-009-9133-x
[15] Botana, F., Montes, A., Recio, T.: An algorithm for automatic discovery of algebraic loci. In: Proceedings of the ADG, pp. 53-59 (2012) · Zbl 1184.68458
[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) · Zbl 1159.68550
[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) · Zbl 1195.68093
[18] Recio, T., Velez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23(1), 63-82 (1999) · Zbl 0941.03010 · doi:10.1023/A:1006135322108
[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) · Zbl 0725.68090
[21] Weispfenning, V.: Comprehensive Gröbner bases. J. Symb. Comput. 14(1), 1-29 (1992) · Zbl 0784.13013 · doi:10.1016/0747-7171(92)90023-W
[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) · Zbl 1053.13013
[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) · Zbl 1321.68533
[24] Montes, A.: A new algorithm for discussing Gröbner bases with parameters. J. Symb. Comput. 33(2), 183-208 (2002) · Zbl 1068.13016 · doi:10.1006/jsco.2001.0504
[25] Montes, A., Wibmer, M.: Gröbner bases for polynomial systems with parameters. J. Symb. Comput. 45(12), 1391-1425 (2010) · Zbl 1207.13018 · doi:10.1016/j.jsc.2010.06.017
[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) · Zbl 1190.13025
[27] Suzuki, A., Sato, Y.: An alternative approach to comprehensive Gröbner bases. J. Symb. Comput. 36(3), 649-667 (2003) · Zbl 1053.13013 · doi:10.1016/S0747-7171(03)00098-1
[28] Weispfenning, V.: Canonical comprehensive Gröbner bases. J. Symb. Comput. 36(3), 669-683 (2003) · Zbl 1054.13015 · doi:10.1016/S0747-7171(03)00099-3
[29] Manubens, M., Montes, A.: Minimal canonical comprehensive Groebner system. J. Symb. Comput. 44(5), 463-478 (2009) · Zbl 1159.13304 · doi:10.1016/j.jsc.2007.07.022
[30] Cox, D., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms, 3rd edn. Springer, New York (2007) · Zbl 1118.13001 · doi:10.1007/978-0-387-35651-8
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.