• GEX

  • Referenced in 33 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 310 articles [sw02904]
  • current automated deduction system Otter is designed to prove theorems stated in first-order 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 ... logic-based approach to geometry theorem proving, a comparison of features of our system with...
  • MMP/Geometer

  • Referenced in 13 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 3 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 high-school 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 169 articles [sw00063]
  • Axiom is a general purpose Computer Algebra system...
  • Cinderella

  • Referenced in 141 articles [sw00127]
  • An Interactive Geometry Software. Besides support for dynamic...
  • CoCoA

  • Referenced in 605 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • Coq

  • Referenced in 1751 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Epsilon

  • Referenced in 39 articles [sw00244]
  • Epsilon is a library of functions implemented in...
  • GAP

  • Referenced in 2702 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • GCLC

  • Referenced in 29 articles [sw00326]
  • We present GCLC/WinGCLC -- a tool for visualizing geometrical...
  • Isabelle

  • Referenced in 598 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • LEDA

  • Referenced in 258 articles [sw00509]
  • In the core computer science areas -- data structures...
  • Macaulay2

  • Referenced in 1576 articles [sw00537]
  • Macaulay2 is a software system devoted to supporting...
  • Maple

  • Referenced in 4919 articles [sw00545]
  • The result of over 30 years of cutting...