GEOTHER 1.1 : Handling and Proving Geometric Theorems Automatically
Identifieur interne : 007A32 ( Main/Merge ); précédent : 007A31; suivant : 007A33GEOTHER 1.1 : Handling and Proving Geometric Theorems Automatically
Auteurs : Dongming WangSource :
English descriptors
- KwdEn :
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.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 003762
- to stream Crin, to step Curation: 003762
- to stream Crin, to step Checkpoint: 000B85
Links to Exploration step
CRIN:wang03bLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="343">GEOTHER 1.1 : Handling and Proving Geometric Theorems Automatically</title></titleStmt><publicationStmt><idno type="RBID">CRIN:wang03b</idno><date when="2003" year="2003">2003</date><idno type="wicri:Area/Crin/Corpus">003762</idno><idno type="wicri:Area/Crin/Curation">003762</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">003762</idno><idno type="wicri:Area/Crin/Checkpoint">000B85</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">000B85</idno><idno type="wicri:Area/Main/Merge">007A32</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">GEOTHER 1.1 : Handling and Proving Geometric Theorems Automatically</title><author><name sortKey="Wang, Dongming" sort="Wang, Dongming" uniqKey="Wang D" first="Dongming" last="Wang">Dongming Wang</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>automated reasoning</term><term>geometry</term><term>theorem prover</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="4091">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.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 007A32 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 007A32 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= CRIN:wang03b
|texte= GEOTHER 1.1 : Handling and Proving Geometric Theorems Automatically
}}
| This area was generated with Dilib version V0.6.33. |  |