GEOTHER 1.1
GEOTHER (GEOmetry THeorem provER), a module of Epsilon, is an environment implemented by Dongming Wang in Maple with drawing routines and interface written previously in C and now in Java for manipulating and proving geometric theorems. In GEOTHER a theorem is specified by means of predicates of the form Theorem(H,C,X) asserting that H implies C, where H and C are lists or sets of predicates that correspond to the geometric hypotheses and the conclusion of the theorem, and the optional X is a list of variables used for internal computation. The information contained in the specification may be all that is needed in order to manipulate and prove the theorem. From the specification, GEOTHER can automatically assign coordinates to each point in some optimal manner; translate the predicate representation of the theorem into an English or Chinese statement, into a first-order logical formula, or into algebraic expressions; draw one or several diagrams for the theorem - the drawn diagrams may be animated and modified with a mouse click and dragging, and saved as PostScript files; prove the theorem using any of the five algebraic provers; translate the generated algebraic nondegeneracy conditions into geometric/predicate form; generate an HTML, LaTeX, and/or PostScript file documenting the theorem and its proof.
Keywords for this software
References in zbMATH (referenced in 30 articles , 1 standard article )
Showing results 1 to 20 of 30.
Sorted by year (- Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
- Davenport, James H.: What does “without loss of generality” mean, and how do we detect it (2017)
- Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon: Automated theorem proving in GeoGebra: current achievements (2015)
- Kovács, Zoltán: The relation tool in GeoGebra 5 (2015)
- Song, Dan; Wang, Dongming; Chen, Xiaoyu: Discovering geometric theorems from scanned and photographed images of diagrams (2015)
- Botana, Francisco; Abánades, Miguel A.: Automatic deduction in (dynamic) geometry: Loci computation (2014)
- Chen, Xiaoyu: Representation and automated transformation of geometric statements (2014)
- Wang, Dongming; Chen, Xiaoyu; An, Wenya; Jiang, Lei; Song, Dan: Opengeo: an open geometric knowledge base (2014)
- Chen, Xiaoyu; Wang, Dongming: Formalization and specification of geometric knowledge objects (2013)
- Chen, Xiaoyu; Huang, Ying; Wang, Dongming: On the design and implementation of a geometric knowledge base (2011)
- Génevaux, Jean-David; Narboux, Julien; Schreck, Pascal: Formalization of Wu’s simple method in Coq (2011)
- Ghourabi, Fadoua; Ida, Tetsuo; Kasem, Asem: Proof documents for automated origami theorem proving (2011)
- Quaresma, Pedro: Thousands of geometric problems for geometric theorem provers (TGTP) (2011)
- Zhao, Ting; Wang, Dongming; Hong, Hoon: Solution formulas for cubic equations without or with constraints (2011)
- Chen, Xiaoyu: Electronic Geometry Textbook: a geometric textbook knowledge management system (2010)
- Escribano, Jesús; Botana, Francisco; Abánades, Miguel A.: Adding remote computational capabilities to dynamic geometry systems (2010) ioport
- Janičić, Predrag: Geometry constructions language (2010)
- Roanes-Lozano, Eugenio; van Labeke, Nicolas; Roanes-Macías, Eugenio: Connecting the 3D DGS Calques3D with the CAS Maple (2010)
- Chen, Xiaoyu; Wang, Dongming: Towards an electronic geometry textbook (2007)
- Janičić, Predrag; Quaresma, Pedro: Automatic verification of regular constructions in dynamic geometry systems (2007)