• OTTER

  • Referenced in 314 articles [sw02904]
  • current automated deduction system Otter is designed to prove theorems stated in first-order logic ... strategies for directing and restricting searches for proofs. Otter can also be used ... logic, group theory, lattice theory, and algebraic geometry. Note: Otter/Mace2 are no longer being actively...
  • GEX

  • Referenced in 35 articles [sw09961]
  • automated prove geometry theorems, to discover new prrperties of theorems, and to generate readable proofs...
  • MMP/Geometer

  • Referenced in 13 articles [sw00584]
  • software package, MMP/Geometer, developed by us to automate some of the basic geometric activities including ... method for Euclidean and differential geometries, the area method and the geometric deductive database method ... theorems and generate short and readable proofs. As a geometric diagram editor, MMP/Geometer ... combining the idea of dynamic geometry and methods of automated diagram generation...
  • HOARD ATINF

  • Referenced in 2 articles [sw28890]
  • Emphasizing human techniques in automated geometry theorem proving: A practical realization. The underlying principles ... Automated Reasoning on your Desk) and has been specialized in this work to proof learning ... through geometry. It is based on a new calculus, particularly suited to the class...
  • EPGY

  • Referenced in 4 articles [sw28722]
  • automated reasoning and symbolic computation to verify individual proof steps. The proof environment has been ... have taken the EPGY high-school geometry course. In addition to providing a general overview...
  • GEOPAR

  • Referenced in 1 article [sw26046]
  • automated realization. A new approach is shown that mechanically proves various theorems in plane geometry ... Python 3 implementation called GEOPAR affords transparent proofs of well-known theorems as well...
  • GeoLogic

  • Referenced in 1 article [sw33592]
  • Euclidean geometry. Domain of mathematical logic in computers is dominated by automated theorem provers ... while ITPs are meant for formalizing existing proofs rather than problem solving ... picked the case study of Euclidean geometry as it can be easily visualized, has simple...
  • ADOL-C

  • Referenced in 239 articles [sw00019]
  • ADOL-C: Automatic Differentiation of C/C++. We present...
  • AXIOM

  • Referenced in 172 articles [sw00063]
  • Axiom is a general purpose Computer Algebra system...
  • Cinderella

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

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

  • Referenced in 1807 articles [sw00161]
  • Coq is a formal proof management system. It...
  • C-XSC

  • Referenced in 108 articles [sw00181]
  • C-XSC. A programming environment for verified scientific...
  • GAP

  • Referenced in 2876 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...
  • GEANT4

  • Referenced in 41 articles [sw00328]
  • Differential elastic hadron-nucleus cross-sections are discussed...
  • Isabelle

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

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

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

  • Referenced in 5957 articles [sw00554]
  • Almost any workflow involves computing results, and that...