Lecture Notes in Artificial Intelligence 6301 EditedbyR.Goebel,J.Siekmann,andW.Wahlster Subseries of Lecture Notes in Computer Science Thomas Sturm Christoph Zengler (Eds.) Automated Deduction in Geometry 7th International Workshop, ADG 2008 Shanghai, China, September 22-24, 2008 Revised Papers 1 3 SeriesEditors RandyGoebel,UniversityofAlberta,Edmonton,Canada JörgSiekmann,UniversityofSaarland,Saarbrücken,Germany WolfgangWahlster,DFKIandUniversityofSaarland,Saarbrücken,Germany VolumeEditors ThomasSturm Max-Planck-InstitutfürInformatik,RG1:AutomationofLogic 66123Saarbrücken,Germany E-mail:[email protected] ChristophZengler UniversitätTübingen Wilhelm-Schickard-InstitutfürInformatik SymbolicComputationGroup 72076Tübingen,Germany E-mail:[email protected] ISSN0302-9743 e-ISSN1611-3349 ISBN978-3-642-21045-7 e-ISBN978-3-642-21046-4 DOI10.1007/978-3-642-21046-4 SpringerHeidelbergDordrechtLondonNewYork LibraryofCongressControlNumber:2011926785 CRSubjectClassification(1998):I.2.3,I.3.5,F.4.1,G.2-3,D.2.4 LNCSSublibrary:SL7–ArtificialIntelligence ©Springer-VerlagBerlinHeidelberg2011 Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,etc.inthispublicationdoesnotimply, evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevantprotectivelaws andregulationsandthereforefreeforgeneraluse. Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) Preface Automated Deduction in Geometry (ADG) 2008 continued an established and fruitful series of biannual international workshops in that area. Previous meet- ings have taken place in Toulouse (1996), Beijing (1998), Zurich (2000), Linz (2002), Gainesville (2004), and Pontevedra (2006). The seventh workshop was held atthe EastChina NormalUniversity (ECNU) in Shanghaiduring Septem- ber22–24,2008.ADG2008wasco-organizedbytheCAS-MPGPartnerInstitute for Computational Biology, the Shanghai Institute of Biology Sciences, and the Chinese Academy of Sciences. While the ADG workshops themselves are quite open also for the informal discussion of work in progress, the selected contributions for the proceedings generally undergo a very thorough and highly selective reviewing process. This publicationintheLNAIseriesofselectedpapersfrom2008continuesatradition established with the first ADG in 1996. As the Chair of the Program Committee, I would like to thank in the first place all PC members, who are listed on the next page, for their competence and dedication during two refereeing processes: first for the workshop contri- butions and then for the selected papers published here; all this comprised a considerabletimespan.Zhenbing Zeng did a perfect job with the localorganiza- tion at the exceptionally interesting location in Shanghai. Manual Kauers and Christoph Zengler greatly supported me with the organization of the online re- viewing process and the preparation of these proceedings. Jesu´s Escribano and Miguel Aba´nades created and maintained a beautiful and informative website, which was most helpful for the organizers as well as for the attendees of the workshop. Last but not least, I particularly want to thank Toma´s Recio and Dongming Wang for their advice that has accompaniedmy organizationalwork for more than two years. March 2011 Thomas Sturm Organization Invited Speakers Shang-Ching Chou Wichita State University, USA/Zhejiang University, China Tetsuo Ida University of Tsukuba, Japan Organizing Committee Zhengbing Zeng Shanghai, China, Chair Miguel A. Aba´nades Madrid, Spain Jesu´s Escribano Madrid, Spain Christoph Zengler Tu¨bingen, Germany Program Committee Thomas Sturm MPI-INF, Saarbru¨cken, Germany, Chair Hirokazu Anai Fujitsu Lab, Japan Francisco Botana Pontevedra,Spain Christopher Brown Annapolis, USA Giorgio Dalzotto Pisa, Italy Jacques Fleuriot Edinburgh, UK Xiao-Shan Gao Beijing, China Hoon Hong Raleigh, USA Deepak Kapur Albuquerque, USA Manuel Kauers Linz, Austria Montserrat Manubens Barcelona, Spain PavelPech Ceske Budejovice, Czech Republic Tom´as Recio Santander, Spain Georg Regensburger Linz, Austria Ju¨rgen Richter-Gebert Munich, Germany PascalSchreck Strasbourg, France Meera Sitharam Gainesville, USA) Dongming Wang Beijing, China/Paris,France Min Wu Shanghai, China Bican Xia Beijing, China Zhenbing Zeng Shanghai, China Table of Contents Contributed Papers Dynamical Systems of Simplices in Dimension Two or Three .......... 1 G´erald Bourgeois and S´ebastien Orange On the Design and Implementation of a Geometric Knowledge Base .... 22 Xiaoyu Chen, Ying Huang, and Dongming Wang Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving ....................................... 42 Benjamin Gr´egoire, Lo¨ıc Pottier, and Laurent Th´ery Multivariate Resultants in Bernstein Basis .......................... 60 Deepak Kapur and Manfred Minimair Unique Factorization Domains in the Java Computer Algebra System... 86 Heinz Kredel Automatic Verification of the Adequacy of Models for Families of Geometric Objects ............................................... 116 Aless Lasaruk and Thomas Sturm Formalizing Projective Plane Geometry in Coq ...................... 141 Nicolas Magaud, Julien Narboux, and Pascal Schreck Linear Programmingfor Bernstein Based Solvers..................... 163 Dominique Michelucci and Christoph Fu¨nfzig Offsetting Revolution Surfaces ..................................... 179 Fernando San Segundo and J. Rafael Sendra An Introduction to Java Geometry Expert (Extended Abstract) ....... 189 Zheng Ye, Shang-Ching Chou, and Xiao-Shan Gao On the Heilbronn Optimal Configuration of Seven Points in the Square.......................................................... 196 Zhenbing Zeng and Liangyu Chen Author Index.................................................. 225 Dynamical Systems of Simplices in Dimension Two or Three G´erald Bourgeois1 and S´ebastien Orange2 1 GAATI,Universit´e dela polyn´esie fran¸caise, BP 6570, 98702 FAA’A,Tahiti, Polyn´esie Franc¸aise [email protected] 2 LMAH, Universit´edu Havre, 25 ruePhilippe Lebon,76600 Le Havre,France [email protected] Abstract. Let T0 =(A0B0C0D0) be a tetrahedron, G0 be its centroid and S be its circumsphere. Let (A1,B1,C1,D1) be the points where S intersects the lines (G0A0,G0B0,G0C0,G0D0) and T1 be the tetrahe- dron (A1B1C1D1). By iterating this construction, a discrete dynamical system of tetrahedra (Ti) is built. The even and odd subsequences of (Ti)convergetotwoisoscelestetrahedrawithatleastageometricspeed. Moreover,wegiveanexplicitexpressionofthelengthsoftheedgesofthe limit. We study the similar problem where T0 is a planar cyclic quadri- lateral.Then(Ti)convergestoarectanglewithatleastgeometricspeed. Finally, we consider the case where T0 is a triangle. Then the even and odd subsequences of (Ti) converge to two equilateral triangles with at leastaquadraticspeed.TheproofsarelargelyalgebraicanduseGr¨obner bases computations. Keywords: Dynamical systems, Gro¨bner basis, Tetrahedron. MSC: Primary 51F, 13P10, 37B. 1 Introduction Notation. Let M,N be two points of Rd. The Euclidean norm of the vector −−→ MN is denoted by MN. 1.1 The General Problem LetT0 =(A0,0···A0,d)bead-simplex,G0 beitscentroid,S beitscircumsphere in Rd, O be the center of S. For all 0 ≤ i ≤ d the line G0A0,i intersects S in two points A0,i and A1,i. Let T1 be the d-simplex (A1,0···A1,d), and G1 be its centroid. If we iterate this process then we produce a dynamical system of d-simplices (Ti)i∈N with centroids (Gi)i∈N. Using Maple,numericalinvestigationswiththousands ofrandomsimplices in dimensions up to 20 indicate that the following results seem true1: 1 Private communication with A. Edmonds(IndianaUniversity). T.SturmandC.Zengler(Eds.):ADG2008,LNAI6301,pp.1–21,2011. (cid:3)c Springer-VerlagBerlinHeidelberg2011