Isometry group, words and proofs of geometric theorems

ABSTRACT

This paper shows that considering the group generated by orthogonal symmetries relatively to lines may give very short and readable proofs of geometric theorems. A short and readable proof of the fundamental Pascal's theorem is provided for illustration.

REFERENCES

• 1: J. E. Bonin. Introduction to matroid theory. The George Washington University. On line.
• 2: S.-C. Chou, Mechanical geometry theorem proving, Kluwer Academic Publishers, Norwell, MA, 1987
• 3: D. Cox, J. Little, and D. O'Shea. Using Algebraic Geometry. Springer-Verlag, New York, 1998.
• 4: N. Dershowitz and D. A. Plaisted. Rewriting. In Handbook of Automated Reasoning, chap 9, vol. 1. Elsevier, 2001.
• 5: M. Henle. Modern Geometries: Non-Euclidean, Projective, and Discrete Geometry. 1997, 2001.
• 6: Y. Martin. Axiomatique de Bachmann: L'approche algébrique ultime pour la géométrie plane. PhD thesis, IUFM de la Réunion, 2002. On line.
• 7: R. Pouzergues. Les hexamys. Technical report, IREM, Nice, 1993. http://hexamys.free.fr/.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Parallel rewriting systems (e.g., developmental systems, L-systems)

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Geometrical problems and computations; Computations on discrete structures; Complexity of proof procedures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Algorithms, Design, Theory

Keywords:
Knuth-Bendix, geometry, groups, involution, isometry, orthogonal symmetries group, rewriting, rewriting methods, words