Abstract
The paper describes proving geometric inequalities in automated way without cell decomposition. Firstly an overview of known methods of proving inequalities is given including the method which is based on reduction of a conclusion polynomial to the canonical form modulo a hypotheses ideal. Then a parametrization method of proving geometric inequalities is introduced. Further a method of proving geometric inequalities which introduces an auxiliary polynomial is described.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bottema, O., et al.: Geometric inequalities, Groningen (1969)
Buchberger, B.: Groebner bases: an algorithmic method in polynomial ideal theory. In: Bose, N.-K. (ed.) Multidimensional Systems Theory, pp. 184–232. Reidel, Dordrecht (1985)
Chou, S.C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Dordrecht (1987)
Chou, S.C., Gao, X.S., Arnon, D.S.: On the mechanical proof of geometry theorems involving inequalities. Advances in Computing Research 6, 139–181 (1992)
Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
Cox, D., Little, J., O’Shea, D.: Ideals, Varieties and Algorithms. Springer, Berlin (1997)
Dalzotto, G., Recio, T.: On protocols for the automated discovery of theorems in elementary geometry. Journal of Automated Reasoning 43, 203–236 (2009)
Gerber, L.: The orthocentric simplex as an extreme simplex. Pacific J. of Math. 56, 97–111 (1975)
Hou, X., Xu, S., Shao, J.: Some geometric properties of successive difference substitutions. Science China, Information Sciences 54, 778–786 (2011)
Kapur, D.: A Refutational Approach to Geometry Theorem Proving. Artificial Intelligence Journal 37, 61–93 (1988)
Mitrinovic, D.S., Pecaric, J.E., Volenec, V.: Recent Advances in Geometric Inequalities. Kluwer Acad. Publ., Dordrecht (1989)
Nelsen, R.: Proofs Without Words. MAA (1993)
Parrilo, P.A.: Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. PhD. thesis. California Institute of Technology, Pasadena, California (2000)
Pech, P.: Selected topics in geometry with classical vs. computer proving. World Scientific Publishing, New Jersey (2007)
Recio, T., Sterk, H., Vélez, M.P.: Project 1. Automatic Geometry Theorem Proving. In: Cohen, A., Cuipers, H., Sterk, H. (eds.) Some Tapas of Computer Algebra, Algorithms and Computations in Mathematics, vol. 4, pp. 276–296. Springer, Heidelberg (1998)
Reznick, B.: Some concrete aspects of Hilbert’s 17th Problem. Contemp. Math. 253, 257–272 (2000)
Wang, D.: Gröbner Bases Applied to Geometric Theorem Proving and Discovering. In: Buchberger, B., Winkler, F. (eds.) Gröbner Bases and Applications. Lecture Notes of Computer Algebra, pp. 281–301. Cambridge Univ. Press, Cambridge (1998)
Wang, D.: Elimination Methods. Springer, Wien (2001)
Wang, D.: Elimination Practice. Software Tools and Applications. Imperial College Press, London (2004)
Weitzenböck, R.: Math. Zeitschrift 5, 137–146 (1919)
Wu, W.-T.: Mathematics Mechanization. Science Press, Kluwer Academic Publishers, Beijing, Dordrecht (2000)
Yang, L., Zhang, J.: A Practical Program of Automated Proving for a Class of Geometric Inequalities. In: Richter-Gebert, J., Wang, D. (eds.) ADG 2000. LNCS (LNAI), vol. 2061, pp. 41–57. Springer, Heidelberg (2001)
Yang, L.: Difference substitution and automated inequality proving. Journal of Guangzhou Univ., Natural Science Edition 5(2), 1–7 (2006)
Yao, Y.: Termination od the sequence of SDS and machine decision for positive semi-definite forms. arXiv:0904.4030v1 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pech, P. (2011). On One Method of Proving Inequalities in Automated Way. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds) Automated Deduction in Geometry. ADG 2010. Lecture Notes in Computer Science(), vol 6877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25070-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-25070-5_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25069-9
Online ISBN: 978-3-642-25070-5
eBook Packages: Computer ScienceComputer Science (R0)