
GEX
 Referenced in 35 articles
[sw09961]
 dynamic diagram drawing and automated geometry theorem proving and discovering. As a dynamic geometry software ... learning of various mathematical concepts. As an automated reasoning software, we can build dynamic logic ... With these methods, users may automated prove geometry theorems, to discover new prrperties of theorems...

OTTER
 Referenced in 316 articles
[sw02904]
 current automated deduction system Otter is designed to prove theorems stated in firstorder logic ... logic, group theory, lattice theory, and algebraic geometry. Note: Otter/Mace2 are no longer being actively...

HOARD ATINF
 Referenced in 2 articles
[sw28890]
 Emphasizing human techniques in automated geometry theorem proving: A practical realization. The underlying principles ... theorem prover are presented. The system (a prototype) is called HOARDATINF (Human Oriented Automated Reasoning ... this work to proof learning through geometry. It is based on a new calculus, particularly ... logicbased approach to geometry theorem proving, a comparison of features of our system with...

MMP/Geometer
 Referenced in 14 articles
[sw00584]
 automate some of the basic geometric activities including geometric theorem proving, geometric theorem discovering ... theorem prover, MMP/Geometer implements Wu’s method for Euclidean and differential geometries, the area method ... only prove difficult geometric theorems but also discover new theorems and generate short and readable ... combining the idea of dynamic geometry and methods of automated diagram generation...

WinGCLC
 Referenced in 5 articles
[sw08574]
 tool for visualizing and teaching geometry, and for producing mathematical illustrations. GCLC provides easy ... transformations, conics, parametric curves, flow control, automated theorem proving, etc. The basic idea behind GCLC...

GEOPAR
 Referenced in 1 article
[sw26046]
 automated realization. A new approach is shown that mechanically proves various theorems in plane geometry...

EPGY
 Referenced in 4 articles
[sw28722]
 Environment for Teaching Mathematics. The EPGY Theorem Proving Environment is a computer program used ... database of theorems, and mathematical rules. The system uses a combination of automated reasoning ... have taken the EPGY highschool geometry course. In addition to providing a general overview ... learned from student use of the Theorem Proving Environment in the EPGY geometry course...

GeoText
 Referenced in 3 articles
[sw12576]
 manage knowledge elements in plane Euclidean geometry. The textbook is dynamic in the sense that ... automated. Supported by a structured and formalized knowledge base, having a geometric theorem prover(GEOTHER ... contents, discovering relations among geometric knowledge data, proving geometric theorems, and generating dynamic diagrams...

GeoLogic
 Referenced in 1 article
[sw33592]
 computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both ... picked the case study of Euclidean geometry as it can be easily visualized, has simple ... pictures. We present our system for Euclidean geometry, together with a graphical application GeoLogic, similar ... which allows users to interactively study and prove properties about the geometrical setup...

AXIOM
 Referenced in 173 articles
[sw00063]
 Axiom is a general purpose Computer Algebra system...

Cinderella
 Referenced in 153 articles
[sw00127]
 An Interactive Geometry Software. Besides support for dynamic...

CoCoA
 Referenced in 654 articles
[sw00143]
 CoCoA is a system for Computations in Commutative...

Coq
 Referenced in 1880 articles
[sw00161]
 Coq is a formal proof management system. It...

Epsilon
 Referenced in 44 articles
[sw00244]
 Epsilon is a library of functions implemented in...

GAP
 Referenced in 3154 articles
[sw00320]
 GAP is a system for computational discrete algebra...

GCLC
 Referenced in 31 articles
[sw00326]
 We present GCLC/WinGCLC  a tool for visualizing geometrical...

Isabelle
 Referenced in 698 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

LEDA
 Referenced in 263 articles
[sw00509]
 In the core computer science areas  data structures...

Macaulay2
 Referenced in 1904 articles
[sw00537]
 Macaulay2 is a software system devoted to supporting...

Maple
 Referenced in 5363 articles
[sw00545]
 The result of over 30 years of cutting...