Automated Deduction in Geometry
AutomatedDeduction inGeometry(ADG) is aseriesofinternationalworkshops where active researchers exchange ideas and views, present research results and progress, and demonstrate software tools on the intersection between geo- try and automated deduction. This volume contains several excellent papers (selected via peer review) based on the talks given at the ADG 2004 meeting hosted by the University of Florida, USA, during September 16–18, 2004. The previous four meetings were held in Linz (2002), Zurich (2000), Beijing (1998), and Toulouse (1996). This volume consists of 12 papers. The paper by Laura I. Meikle andJacques D. Fleuriot shows how to prove the correctness of an algorithm for comp- ing convex hulls, by using Hoare logic and Isabelle. The paper by Judit Robu, Tetsuo Ida, Dorin T ¸epeneu, Hidekazu Takahashi,and Bruno Buchberger shows how to prove the correctness of an origami construction (heptagon), by using the Theorema system and Gr¨ obner bases. The paper by Xuefeng Chen, Peng Li, Long Lin,and Dingkang Wang shows how to treat degenerate cases in geom- ric theorems rigorously, by introducing partitioned-parametric Gr¨ obner bases.
All current issues in the area are addressedCovers theoretical and methodological topics as well as applications thereof Includes an particular automated geometry theorem proving, automated geometry problem solving, problems of dynamic geometry, and an object-oriented language for geometric objects.