This is supposed to be a fairy complete overview of current systems (and projects) implementing "mathematics in the computer".

In order to qualify for this list a system has:

• to be about mathematics
  so for instance a word processor will qualify for this list only if it is a mathematical word processor: which means that TeX qualifies and Word doesn't
• to have something to do with computers
  a project doesn't necessarily have to produce software to qualify: a standard for encoding math - like OpenMath - or a project with nice ideas - like QED - are in this list too
• to be significant
  it has to produce software, or some kind of sizable collection, or some interesting idea, or a large group of people have to be involved, etc.
• to be public
  it should be possible to acquire the system: by way of the internet, or by buying it, or by contacting the author, etc.
• to be active
  at the very least there has to be some web page about it that this list can point to

If this list can be improved, either because a relevant system is missing, or because the information about some system is wrong (for instance, a link to a web page might no longer work), or because there is a better web page to point to than the one that's in the list, then I'd very much would like to know. In that case please send mail to freek@cs.kun.nl.

For each system this overview contains the following information:

• the name of the system
• the name of the program implementing the system (if appropriate)
  for instance there are quite a number of programs implementing the HOL system; similarly there are a great number of MACSYMA derivates with all kinds of names; often not all implementations are in this overview: I restricted myself to the most "active" or the most "interesting" (to me) of the implementations; generally the other implementations can easily be found on the web page about the system
• the URL of a web page or ftp site about the system
• an e-mail address that can be used to contact the project that produced the system
• the name (or names) of the principal architect of the system
  if there have been more people than just the architect(s) significantly involved in the writing of the software the name is followed by "e.a."; by "architect" I don't mean the person who "designed" the the system, nor the (current) leader of the project, but the principal programmer: the one who took the main design decisions of the detailed implementation of the software; for instance for the current coq implementation this seems to be Chet Murthy
• the programming language the system is implemented in
• the name of the specific variant of this programming language (if appropriate)
  for instance "lisp" might be "franz lisp" or "common lisp" or "scheme", etc.
• the category of the system
  see below for a list (and explanations) of the various categories
• the kind of interaction the system has with the user
  see below for a list (and explanations) of the various kinds of interaction
• the kind of logic the system uses
  there are four choices: none, classical, constructive and both
  here the kind of logic that is commonly used in the system is shown: for instance in coq one can easily reason classically by taking the double negation rule as an axiom, but because most of the applications of coq don't do this, coq is labeled "constructive"; similarly although Automath has a type theoretical foundation the large case studies in the Automath project were all classical: hence Automath is labeled "classical"; only if in a system both kinds of logic have been significantly developed, like for instance in the Isabelle system, then it will be labeled "both"
• the size of the effort that produced the system
  there are three choices: small, large and commercial
  the first two options are only used for non-commercial systems
  a small system generally only involves one or two people; the home page of such a system is generally "in" the home page of its main author; the distribution of such a system is generally at most a megabyte in size
  a big system generally has been active for years; it generally involves a group of tens of people; such a system often has its own mailing list or newsgroup; such a system often has a number of different implementations; the distribution of such a system often is tens of megabytes in size
• a sample of the language used within the system
  I selected these samples in the following way: I looked for the biggest relevant "example" file from the distribution that I could find; in that file I went to the last of lines number 42, 137 and 666 that was present; and starting from that line I took a sample of 24 lines

Each system in this list falls in one of nine categories. All but the first two categories are for projects that produce software. The "non software" categories are:

• information
  example: the QED project
  this is for lists like this, bibliographies, people talking without doing anything, etc.
• representation
  example: the OpenMath project
  this is for languages/standards for encoding/exchanging mathematics
  large collections of problems (used as a "benchmark" to compare first order theorem provers) are in this category too

The "mathematics software" is categorized into five main categories:

• authoring
  example: TeX
  these are the typesetting systems, the authoring tools, etc.: software that encodes/processes mathematics to communicate it to other humans, but doesn't process it "mathematically"
• computer algebra
  example: Mathematica
  these are the symbolic "calculators"; generally they don't have a very rigorous mathematical foundation, nor do they have much reasoning capacities; generally they implement very powerful and complicated algorithms to calculate mathematical expressions
  there are various kind of computer algebra systems: for numerical calculations, for doing "calculus"-like mathematics, for doing abstract algebra, etc.: I don't distinguish between those subcategories
• proof checker and theorem prover
  examples: mizar and nqthm
  these two categories are closely related: both are about "mechanical reasoning": the difference is whether the focus is on the computer checking the reasoning of the human, or on the human watching and guiding the computer's proof efforts; the more a system tries to be "smart", the more chance it has of being in the "theorem prover" category
  there are two kinds of theorem provers that have been put in two separate categories of their own (see below): so the "theorem prover" category might have better been called "other theorem prover"
• specification environment
  example: obj
  these are theorem provers too in a sense, but highly specialised ones which are used to specify and verify computer systems: so the focus here is not so much on trying to do mathematics as well as on the correctness of software
  a system in this category has only been put in the list if it explicitely mentions something like logic or mathematics or automated reasoning on its web page: for instance the asf+sdf system isn't there

There are three kinds of proof checkers and theorem provers that have a category of their own:

• logic education
  example: hyperproof
  this is the class of proof checkers which are intended to teach logic to students
• tactic prover
  example: coq
  these systems are often called "proof assistants"
  these systems are descendants of the LCF system, generally based on a higher order and type theoretical foundation and often implemented in the ML programming language
  in this kind of system something is proven interactively by a user invoking so-called "tactics" on a partially solved "proof goal"
• first order prover
  example: otter
  this is a highly specialised class of theorem provers, which often use clausal forms for their problems, there are competitions between the various members of this category to see which one is best, etc.

The interaction with a mathematical program has two orthogonal dimensions:

• either the user prepares a file and then runs the program on that file; or else the user has significant interaction with the program while it is running
• either the files that the user creates contain a sequence of commands for the "read-eval-print loop" of the program (so it is a "script", maybe called a "notebook"); or else the file contains something more intricate than just a sequence of commands to the program

These two dimensions lead to four kinds of interaction:

• dialog: interaction + command file
• editor: interaction + non-command file
• script: non-interaction + command file
• batch: non-interaction + non-command file

A program is classified by its most common mode of producing texts: for instance coq can be used in the dialog way ("coqtop") and the script way ("coqc"): but because people most often write coq proofs by copying fragments between an editor and a running coq interpreter, it's classified "dialog".

I probably made some mistakes in distinguishing between "dialog" and "script" systems.

Apart from these four kinds of interaction, there are three kinds of "non interaction" too:

• library:
  this is software that isn't a finished program but a "software library" that can be linked to other people's programs
• interface:
  here the software is about interfacing between other software: so it doesn't so much do something itself as well as communicates with other programs
• corpus:
  in this case there is no software at all, but just a "static" collection of data, for instance like in the "benchmarks" for the first order provers

(last modification 1999-01-18)