cs2054 - Symbolic Computer Algebra Systems, Mathematical Proof Assistants, and other Mathematical Engines

cs2054 - A collection software packages for manipulation of Mathematical Symbology with the aid of a computer. Many of the packages also have impressive numerical capabilities, but this is not the emphasis of this collection. Copyright 2006 Edition Arnold Kochman. Other copyrights apply, including but not limited to the GNU Public License. 

  

Users will need one of the commonly available unzip type utilities, such as PKUNZIP or WinZip, tar for Linux, etc. Programs are distributed with source, when appropriate, and some programs in C, for example, will have to be compiled.

The various packages are at different levels of maturity and sophistication, and naturally I cannot certify that they are all worthwhile for any particular purpose.

Here is a listing of the packages included:

Mathematics Engines, Symbolic
MathEclipse - A symbolic mathematics engine written in Java and JavaScript with a parser/pattern matcher similar to the Mathematica language. MathEclipse is an AJAX based symbolic mathematics calculator and plugin for the Eclipse Framework. Eclipse and MathEclipse are written in Java, and will run on all graphical desktop environments which support Java. MathEclipse is available under the Common Public Licence. MathEclipse supports rule based pattern-matching programming, big numbers in Integer, Complex, and Rational objects, double precision for Real and ComplexReal, list manipulation, and a math expression parser. It runs on Windows 95/98/NT/2000/XP, and Linux/BSD/UNIX systems.
Math.NET - A framework for symbolic mathematical and numerical/scientific computations, including a parser and support for linear algebra, complex differential analysis, system solving and more. Math.NET is written in C# and it runs on Windows 95/98/NT/2000/XP/CE. The maker seems to represent that it runs under under Linux/BSD/UNIX systems as well, but skepticism on this point seems warranted. It is distributed under the BSD License, the GNU General Public License, and the GNU Library or Lesser General Public License.
SymDiff - A command line tool for symbolic differentiation and expression evaluation. The code can be used for the symbolical implementation of certain mathematical algorithms that require derivatives. It is written in C and C++ and is distributed under the terms of the GNU General Public License.
HartMath - An experimental computer algebra program written in Java. It features big number arithmetic, symbolic and numeric evaluation, plot-, polynomial-, vector, and matrix-functions. It is written in Java and runs on 32 bit Windows systems, UNIX/Linux/BSD systems with X11, MaxOS X, and similar systems. It is released under the GNU General Public License.
Kalamaris - A mathematics research framework created by Antonio Larrosa. It is similar to Mathematica in some aspects, but offers a new approach to solve mathematical problems and simulate physics models easily. Kalamaris is a KDE application and therefore should be considered applicable only to UNIX/Linux systems. Kalamaris' main features are: Function definition and evaluation, plotting functions in 2D, matrix support, symbolic calculus, symbolic derivatives, numerical solution of systems of differential equations, and data visualization in a 3D viewer. 
PARI/GP - A package aimed at efficient computations in number theory, written by Karim Belabas. It is approximately a Computer Algebra System, but not precisely since it treats symbolic expressions as mathematical entities such as matrices, polynomials, series, etc., and not as expressions per se. However it is often much faster than other CAS, and contains a large number of specific functions not found elsewhere, essentially for use in number theory. There is a GP to C compiler to translate GP scripts to PARI programs. 
Yacas - Yet Another Computer Algebra System - Yacas is a general purpose, easy to use Computer Algebra System. It is based upon its own programming language designed for this purpose, in which new algorithms can easily be implemented. In addition, it comes with extensive documentation on the functionality implemented and methods used to implement them. Yacas is written in C++ and runs chiefly on Windows and Linux/UNIX systems. Versions for some other operating systems exist, but appear not to be vigorously supported, and are not included. Yacas is distributed under the GNU General Public License.
jscl-meditor - A Java symbolic computing library and math editor, written by Raphael Jolly. It includes polynomial system solving, vectors and matrices, factorization, derivatives, integrals (rational functions), boolean algebra, simplification, MathML output, Java code generation, and geometric algebra. It is distributed under the GNU Lesser General Public License.
libmatheval - GNU libmatheval is a library to parse and evaluate symbolic expressions input as text, written by Aleksandar B. Samardzic. It supports expressions in any number of variables of arbitrary names, decimal constants, basic unary and binary operators, and elementary mathematical functions. In addition to parsing and evaluation, libmatheval can also compute symbolic derivatives and output expressions to strings. GNU libmatheval is written in C and FORTRAN and is suitable for UNIX/Linux systems. Modules can be linked to C and FORTRAN programs. It is released under the terms of the GNU General Public License.
GiNCa - A program designed as a replacement engine for xloops which in the past was powered by the Maple CAS. Contrary to other CAS it does not try to provide extensive algebraic capabilities and only secondarily a programming language. Rather, a programming language (C++) is taken as a given, and GiNCa extends it with a repetoire of algebraic capabilities. GiNaC is written in ANSI-C++, i.e. adhering to the international standard ISO/EIC 14882-1998(E). using the Gnu Compiler Collection (GCC). It should run on any system, where a reasonably contemporary GCC is installed. This includes most Unix variants (Linux, Solaris, Tru64,...) and also Machines running Windows if cygwin is used as a compiler. GiNCa is distributed under the GNU General Public License.
SINGULAR - A Computer Algebra System for polynomial computations with special emphasis on the needs of commutative algebra, algebraic geometry, and singularity theory. SINGULAR implements a large variety of algorithms. It is extensively documented and is available for Linux/UNIX/HP-UX/SunOS/Solaris/AIX, Windows, and Macintosh. A Mac OS X version is not included in this distribution; it can be downloaded from "The Fnk project". SINGULAR is distributed under the GNU General Public License.
Macaulay 2 - A software system devoted to supporting research in algebraic geometry and commutative algebra, whose development has been funded by grants from the National Science Foundation (USA). Macaulay 2 is copyright 1993-2002 by Daniel R. Grayson and Michael E. Stillman, and is made available under the terms of the GNU General Public License, version 2. Macaulay 2 is written in C and C++, and is suitable to run on Linux and OS X systems. 
Maxima - A system for the manipulation of symbolic and numerical expressions, including differentiation, integration, Taylor series, Laplace transforms, ordinary differential equations, systems of linear equations, and vectors, matrices, and tensors. Maxima produces high precision results by using exact fractions and arbitrarily long floating point representations, and can plot functions and data in two and three dimensions.
    Maxima is a descendant of Macsyma, the legendary computer algebra system developed in the late 1960s at the Massachusetts Institute of Technology. Macsyma was revolutionary in its day, and the inspiration for systems, such as Maple and Mathematica. The Maxima branch of Macsyma was maintained by William Schelter from 1982 until he passed away in 2001. In 1998 he obtained permission to release the source code under the GNU General Public License (GPL). Maxima is written in C and Lisp, and runs on Linux/BSD/UNIX type systems with X11. There is also a Windows program.
AXIOM - A general purpose Computer Algebra system. It is useful for doing mathematics by computer and for research and development of mathematical algorithms. The Axiom Language provides a very high-level way to express abstract mathematical concepts that are collected in the Axiom Library which defines over 1,000 strongly-typed mathematical domains and categories.
    The AXIOM symbolic solver is no longer available from NAG (The Numerical Algorithms Group). Release 2.3, made available in March 2001 to sites already licensed to use AXIOM, was the last update produced. However, NAG has released the source code to a consortium of AXIOM users and developers who have created a version which is available under the Modified BSD license. Axiom has an active users' group.
Giac/Xcas - A computer algebra system for Windows, Mac OS X and Linux/Unix. It has compatibility modes for Maple, MuPad and the TI89. It is available as a standalone program (graphic or text interfaces) or as a C++ library. Documentation exists in English, but the best documentation is in French. Windows users will need to assure that suitable versions of Ghostview and GSview are installed.
MAS - Modula-2 Algebra System - An experimental computer algebra system, developed at the University of Passau. MAS combines imperative programming facilities with algebraic specification capabilities for design and study of algebraic algorithms. It contains a large library of implemented Groebner basis algorithms for nearly all algebraic structures where such methods exist. MAS further includes algorithms for real quantifier elimination, parametric real root counting, and for computing in (noncommutative) polynomial rings.
Felix - A special computer algebra system for computation in commutative and non-commutative rings and modules, written by Joachim Apel and Uwe Klaus. The central method is Buchberger's algorithm and its generalizations to non-commutative rings, in particular to free k-algebras and algebras of solvable type. Among the implemented applications there are syzygy computations and basic ideal operations. Felix provides a complete programming language which in standard mode is interpreted. However, a compiler and linker are also included. Felix runs on Windows, Windows NT, OS/2, Linux, NetBSD, and Solaris. Only binaries are available.
Albert - An interactive program to assist the specialist in the study of nonassociative algebra. The program was first designed and implemented at Clemson University about 1990 by D. Jacobs and S.V. Muddana, with assistance from A.J. Offutt. Enhancements have been made by K. Prabhu, D. Lee, and T. Whiteley. The main problem addressed by Albert is the recognition of polynomial identities in varieties of nonassociative algebras. Albert is written in C and runs on UNIX. It is distributed persuant to the GNU General Public License.
Bertrand - A symbolic logic problem-solving program, written by Larry A. Herzberg for the classic Macintosh operating system. 
Coq - The Coq proof assistant - The Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. It was developed in the LogiCal project. Coq allows: the definition of functions or predicates; statement of mathematical theorems and software specifications; interactive development of formal proofs; and checking of these proofs by a certification module. Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories. Coq includes a graphical user interface, a documentation tool, and a preprocessor for TeX files that include Coq commands.
    Coq is written in the Objective Caml language and uses the Camlp4 Pre-processor-pretty-printer for Objective Caml. Coq is distributed under the GNU Lesser General Public Licence Version 2.1 (LGPL). It available for UNIX (including Mac OS X) and Windows 95/98/NT/XP systems.
Isabelle - A generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols. Isabelle's distinguishing feature is its flexibility. Most proof assistants are built around a single formal calculus, typically higher-order logic. Isabelle has the capacity to accept a variety of formal calculi. The distributed version supports higher-order logic but also axiomatic set theory and several other formalisms. See logics for more details.
    Isabelle is a joint project between Lawrence C. Paulson (University of Cambridge, UK) and Tobias Nipkow (Technical University of Munich, Germany). Isabelle is distributed under the BSD license.
JACAL - An interactive symbolic mathematics program. JACAL can manipulate and simplify equations, scalars, vectors, and matrices of single and multiple valued algebraic expressions containing numbers, variables, radicals, and algebraic differential, and holonomic functions. For UNIX and Windows. JACAL is released under the GNU General Public License.
Mathomatic - A portable, general purpose Computer Algebra System, written entirely in C by George Gesslein II. This is a console mode application and library that quickly and easily compiles and runs under any operating system with a C compiler. There are no dependencies other than the standard C libraries. Mathomatic is designed to be as general and easy to use as possible, and as such, has no programming capability. It implements most of the rules of algebra for the mathematical operators +, -, *, /, modulus, and power (including roots). All arithmetic is double precision floating point. Mathomatic can symbolically: solve equations; simplify and compare equations; derivatives, integrals, and Laplace, and Taylor transforms; and carry out a variety of computational tasks. Furthermore, it can generate efficient C, Java, or Python code from equations. Mathomatic is released under the GNU Lesser or Library general Public License.
Otter - An automated deduction system designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be used as a symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP. Otter is written in ANSI C; it has been used primarily on UNIX type systems, but limited versions also run in Microsoft Windows.
    Otter and MACE automated deduction software was developed at Argonne National Laboratory under a U.S. Government contract and is subject to the following license: the Government is granted for itself and the public a paid-up, nonexclusive, irrevocable worldwide license in this material to reproduce, prepare derivative works, distribute copies to the public, and perform publicly and display publicly.