ACA'2002, June 25-28, 2002, Volos, Greece

Session on 
in elementary geometry

Organized by  Tomas Recio 
(Universidad de Cantabria)  


This session will be devoted to present some of my  favourite trends on Automatic Geometry Theorem Proving:

  • Applications to Computer Aided Geometric Design, through Geometric Constraint Solving (see abstracts no. 2 and 6 below)
  • Applications to education, cooperation with dynamic geometry software (see abstracts no. 1 and 5 below)
  • New results and methods on the algebrization of Geometry Theorem proving and discovery (see abstracts no. 3, 4 and 7 below)
  • Hopefully, besides the invited speakers, there will be time for a few submitted contributions as short talks.  
    You are welcome to submit your work on the topic!

    For more information and/or to present a paper at the session, please contact the session organizer by e-mail.

    Confirmed invited speakers (in alphabetic order):

       1- Francisco Botana (U. Vigo, Spain)

              Automatic determination of plane loci
                       (joint work with J.L. Valcarce)

    This talk will describe a successful implementation of a software tool for determining plane loci using the Groebner basis method. The program consists of a graphical interface linking a standard dynamic geometry environnment and a computer algebra system. The user can do any ruler and compass construction and impose geometric conditions to some elements of the construction in order to get the locus of a point. The dynamic geometry module translates its geometric knowledge into an algebraic one, and exports it to a computer algebra system (CoCoA or Mathematica), where it is carried out an elimination process. The result of this elimination includes the locus polynomial. This locus is then returned twofold: as the implicit equation of the algebraic curve and as a graphic object in the screen.
    Apart from the obvious implications for mathematics education, the program can be used for geometric discovery, linkage design and testing, computer aided geometric design and related fields. Some experimental improvements of the software, such as generating dynamic loci and returning loci which are semialgebraic sets, will also be discussed.

    A demo can be downloaded at

        2-Robert Joan-Arinyo (U. Politécnica de Catalunya, Barcelona)

             Ruler and compass geometric constraint solving

    Geometric constraint solving techniques have received considerable attention in recent years. The problem is to take as input an sketch of a geometric drawing annotated with geometric constraints like distances between points, angles between straight lines, tangencies between lines and circles and so forth, and either generate  a drawing that actually fulfills the set of constraints or determine that such a geometric object does not exists.
    This talk will focus on the ruler-and-compass based,constructive
    geometric constraint solving approach. After reviewing the data
    representation and the constructive rules considered, we will
    characterize the method as a rewriting system. The questions of termination and confluence will be considered.  Then we will show how the constructive technique can be easily combined with equational techniques without mapping one problem domain to the other.  A  practical demo on the BCNsolver prototype developed by our group will close the talk.

      3-Deepak Kapur (U. New Mexico, Albuquerque, USA)
           Geometric Reasoning and Dixon Resultants

    Recent results on the generalized Dixon resultant formulation proposed by Kapur, Saxena and Yang (ISSAC'94) will be reviewed. Conditions on multivariate polynomial systems for which the Dixon formulation computes the resultants exactly will be discussed. In many cases, the degree of the extraneous factor in the projection operator computed using the Dixon resultant formulation can be predicted as well. These results have implications for geometry theorem proving.
    A construction for Sylvester-like matrices based on the generalized resultant formulation for simultaneously eliminating many variables from a polynomial system will be discussed. This construction has found to be especially effective for mixed polynomial systems.


        4- Hongbo Li (Institute of  Systems Science, Chinese Academy of Sciences, Beijing, China)

         Short Proof Generation with Cayley Algebra and Bracket    Algebra.

    Cayley algebra and bracket algebra are an important approach to automated theorem proving in projective geometry. Recently we established the Cayley expansion theory on factored and 
    shortest expansions of typical Cayley expressions. Based on the
    classification of these expansions, we set up a group of Cayley factorization formulas and simplification techniques in bracket 
    computation. These techniques contribute to producing extremely short proofs for projective geometric theorems ( 

    Furthermore, by studying different representations of geometric
    constructions and relations in projective conic geometry with Cayley algebra and bracket algebra, we came up with several powerful  simplification techniques for bracket computation involving conic points, and an algorithm for  rational Cayley factorization. By these techniques, we can produce extremely short proofs for difficult theorems in conic geometry. Our central idea to generate readable proofs in projective geometry is "BREEFS'' -- Backet-oriented Representation, Elimination and
    Expansion for Factored  and Shortest results (

       5- Nicolas Peltier (CNRS- IMAG, Grenoble, France)

    HOARD-ATINF: a Logical Theorem-Prover for Teaching Proof 
    in  Geometry

    There is still an important gap between Automated Deduction tools and their use for educational purpose, particularly for young students. The reason is that automated reasoning systems should be able not only to construct proofs, but also to integrate most of the features that play a central role in the human way of thinking. These features are often neglected by existing systems. Ideally, an ATP aimed to be used in educational tasks should include, for example, the following features:
      -Good presentation of proofs. In particular, the level of details of the proof and the considered axiomatisation (available axioms and theorems) should be flexible and should depend on the level of knowledge of the student.
      -Automated verification of the student's proofs
      -Automated construction of counter-examples (for disproving conjectures, helping a student to correct wrong intuitions etc.).
      -Automatic detection of analogies between formulae and/or proofs.

    The gap is even more important in the field of Geometry. Indeed, the most powerful geometry theorem provers are based on algebraic approaches, which makes the integration of such  "advanced'' features very difficult.

    The ( Baghera project (presently developed in a framework of a european cooperation) intends to develop theoretical and methodological foundations to guide the computer modelling and conception of learning environments. The chosen domain knowledge is the teaching of proof in Geometry.
    In this talk we will focus essentially on the automated reasoning part of the Baghera plateform.
    We will describe the Theorem Prover HOARD-ATINF (specially developed to be used in this project), its theoretical basis and main fonctionalities.
    HOARD-ATINF is a generic prover, based on a logical calculus including equality. It incorporates several features useful in helping educational agents to analyse student's proofs or to propose alternative proofs.
    The interested reader can see here for
    additional details about the ATINF project.

    6- Meera Sitharam (University of Florida, USA)

    Outstanding Problems in Geometric Constraint Solving:
    approaches and connections to geometry theorem proving.

    After a brief introduction to geometric constraint solving and its many applications, we introduce a list of  key  issues that geometric constraint solvers need to address, and describe briefly how our geometric constraint solver FRONTIER addresses some of  them.  Outstanding issues are how to deal with:
              (i)   ambiguities and inconsistencies in the input constraint system
              (ii)  soft constraints
             (iii)  parameterless constraints.
    To deal with these, we suggest  initial approaches that leverage FRONTIER's existing advantages. We also indicate how these issues overlap with automated (or at least computer assisted) geometry theorem proving.


      7- Dingkang Wang (Institute of  Systems Science, Chinese Academy of Sciences, Beijing, China)

    The projection of quasi varieties and its application on geometry theorem proving

    In this paper, we present a projection method whereby not only 
    to prove whether a given geometric theorem is true, but also to obtain the sufficient and necessary conditions under which the theorem is true, if such conditions exist. This method also can be used to geometric formula deduction. The detail algorithm has been implemented and several  examples are reported in this paper to show the algorithm of practical value.

    Papers presented at the session will be considered for publication at a special issue of the Journal of Symbolic Computation titled Applications of Computer Algebra. The call for papers is available.