First steps on using OpenMath to add proving capabilities to standard dynamic geometry systems. (English) Zbl 1202.68487

Kauers, Manuel (ed.) et al., Towards mechanized mathematical assistants. 14th symposium, Calculemus 2007, 6th international conference, MKM 2007, Hagenberg, Austria, June 27–30, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73083-5/pbk). Lecture Notes in Computer Science 4573. Lecture Notes in Artificial Intelligence, 131-145 (2007).
Summary: A prototype for a web application designed to symbolically process locus, proof and discovery tasks on geometric diagrams created with the commercial dynamic geometry systems Cabri, The Geometer’s Sketchpad and Cinderella is presented. The application, named LAD (acronym for Locus-Assertion-Discovery) and thought of as a remote add-on for the considered DGS, follows the Gröbner basis method relying on CoCoA and a Mathematica kernel for the involved symbolic computations. From the DGS internal textual representation of a geometric diagram, an OpenMath (i.e. semantic-based) description of the requested task is created using the elements in the plangeo OpenMath content dictionaries. A review of the elements included in these CDs is given and two new elements proposed, namely locus and discovery. Everything is finally thoroughly illustrated with examples. LAD is freely accessible at http://nash.sip.ucm.es/LAD/LAD.html.
For the entire collection see [Zbl 1119.68011].


68W30 Symbolic computation and algebraic computation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
Full Text: DOI