Introduction

Linkages and mathematics have developed, along centuries, a tight relation. For instance, drawing curves (as simple as straight lines) with the help of mechanisms can be a challenging issue, in which linkages and mathematics have worked along since long: from the times of Euclid's geometry of the compass to, say, the recent work of Kapovich and Millson for a proof of a conjecture by W. Thurston on the universality of linkages, involving some tools developed by J. Nash in this proof.[br][br]On the other hand, dynamic geometry software is specially well suited to model linkages. In fact, dragging is one of the most characteristic dynamic geometry features, and the same can be stated for bar-joint linkages. Linkage mechanisms are not made to stand still! Thus, there is an ample variety of repositories, web accessible, displaying many different linkages by dynamic geometry applets. [br][br]As it is well known, dynamic geometry programs have been used until now, mainly, as computer environments for studying school geometry. In particular, the didactical possibilities of using mechanical linkages in dynamic geometry environments have been already noticed for a long time. But in this talk we will go in a different direction and refer to the recent implementation of tools for the automatic proving, derivation and discovery of geometric theorems over GeoGebra. [br][br]In this context, the purpose of our paper is to describe some on-going work on the crossroad of mechanical linkages, dynamic geometry and automatic reasoning tools. In particular, we shall consider how these new tools can be used for linkage exploration, i.e. for[br][br][list][*]the automatic derivation of the locus equation for some relevant moving point in a linkage (e.g. linkages for generating specific algebraic curves, such as Peaucellier's construction of a straight line), and, in this way, for [br][/*][*]the verification (automatic proving) of the correctness of the linkage construction, as well as, for [br][/*][*]finding (automatic discovery) a suitable modification on a given linkage for achieving a desired movement.[/*][/list][br]By "automated proving, derivation or discovery of geometry statements" we refer to the mechanically output of a mathematically rigorous (e.g. not based upon a probabilistic proof) yes/no answer to the conjectured truth of a given (or observed) geometric statement, or to automatically finding complementary, necessary, hypotheses for a conjectured geometric statement to become true. Briefly, this is achieved by considering, as extra hypotheses, the equations of the locus of a given point in the associated construction, subject to a certain constraint. In all cases, algebraic geometry algorithms are called and executed through symbolic algebraic computations performed by Giac, the Computer Algebra System embedded in GeoGebra.

Information