GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically

Dongming Wang 1, 2
1 SPACES - Solving problems through algebraic computation and efficient software
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 CALFOR - Calcul formel
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : GEOTHER provides an environment for handling and proving theorems in geometry automatically. In this environment, geometric theorems are represented by means of predicate specifications. Several functions are implemented that allow one to translate the specification of a geometric theorem into English and Chinese statements, into algebraic expressions, and into logic formulas automatically. Geometric diagrams can also be drawn automatically from the predicate specification, and the drawn diagrams may be modified and animated with mouse click and dragging. Five algebraic provers based on Wu's method of characteristic sets, the Gröbner basis method, and other triangularization techniques are available for proving such theorems in elementary (and differential) geometry. Geometric meanings of the produced algebraic nondegeneracy conditions can be interpreted automatically, in most cases. PostScript and HTML files can be generated, also automatically, to document the manipulation and machine proof of the theorem. This paper presents these capabilities of GEOTHER, addresses some implementation issues, and reports on the performance of GEOTHER's algebraic provers.
Type de document :
Communication dans un congrès
Franz Winkler. The Fourth International Workshop on Automated Deduction in Geometry - ADG 2002, Sep 2002, Hagenberg Castle, Austria. Springer-Verlag, 2930, pp.194-215, 2003, Lecture Notes in Computer Science. 〈10.1007/978-3-540-24616-9_12〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00107637
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 09:03:42
Dernière modification le : vendredi 23 février 2018 - 11:19:23
Document(s) archivé(s) le : mercredi 29 mars 2017 - 12:58:07

Identifiants

Collections

Citation

Dongming Wang. GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically. Franz Winkler. The Fourth International Workshop on Automated Deduction in Geometry - ADG 2002, Sep 2002, Hagenberg Castle, Austria. Springer-Verlag, 2930, pp.194-215, 2003, Lecture Notes in Computer Science. 〈10.1007/978-3-540-24616-9_12〉. 〈inria-00107637〉

Partager

Métriques

Consultations de la notice

145

Téléchargements de fichiers

82