ACA'2002,
June 25-28, 2002, Volos, Greece
Session
on
AUTOMATIC
THEOREM PROVING
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:
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
http://rosalia.uvigo.es/sdge/lugares
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 (http://www.mmrc.iss.ac.cn/annal/li1.ps).
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 (http://www.mmrc.iss.ac.cn/annal/li2.ps).
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 (http://www-baghera.imag.fr)
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
http://www-leibniz.imag.fr/ATINF/Welcome-ENG.html
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
http://www.cise.ufl.edu/~sitharam
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.