
OTTER
 Referenced in 314 articles
[sw02904]
 current automated deduction system Otter is designed to prove theorems stated in firstorder 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 highschool 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 wellknown 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...

ADOLC
 Referenced in 239 articles
[sw00019]
 ADOLC: 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...

CXSC
 Referenced in 108 articles
[sw00181]
 CXSC. 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 hadronnucleus crosssections 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...