My homepage | My math page | My math news | Donate for the research

Software for 21 Century Math Method

We are to develop software for 21 Century Math Method^TM (21MM^TM).

Licensing

This software will be simultaneously licensed under GPL and under (new) BSD License to allow its not only non-commercial but also commercial use. A more restrictive licensing of the base of all future mathematics would be a moral crime (except of the case if one would decide to stop the development of science of the mankind for a good reason, but this in not the case).

Requirements

This planned software should have the following features:

implement validation of theorem proofs in 21MM;
powerful automatic finding a proof for a given theorem;
automatic constructing a set of important concepts and relations between concepts after reading a mathematical text (automatic student);
automatic expression simplification;
working with algorithms (see here):
- executing algorithms;
- verifying algorithms;
- transforming algorithms;
convenient input and output of mathematical information;
transforming between old quantifier based mathematical notation and the 21MM notation;
have bridge to standalone programming languages such as C and Ada95.

Additionally this software is to be accompanied with a big database of mathematical knowledge.

This software is to take simultaneously the functions similar to the following existing softwares:

Mathematica (a system for automatic problem solving and expression simplification).
Mizar (a system for writing mathematical knowledge in computer form with automatic theorem proving). However Mizar uses a formalized variant of 20 century mathematical vernacular while we are instead reformalizing the mathematics in a new more algebraic formalistic which is essentially to replace the vernacular in fundamental applications. Eventually we should be able to translate from Mizar's vernacular into our algebraic formal notation.

We are to eventually surpass these softwares.

Planned Implementation

I plan to implement it in Ada95 programming language.

For simplicity we will use a little different data structure for expressing formulas, than in the current version of the article (5 May 2005). Here is simplified (without reference counting and without optimization) Ada code for formulas :

package Formulas is

   --- Symbols ---

   type Symbol_Type is private;

   function "="(Left: Symbol_Type; Right: Symbol_Type) return Boolean;

   --- Formulas and lists of formulas ---

   type Formula_List_Type;

   type Formula_Type is
      record
         Symbol   : Symbol_Type;
         Arguments: Formula_List_Access;
      end record;

   type Formula_Access is access Formula_Type;

   type Formula_List_Type is
      record
         Formula: Formula_Access;
         Next   : Formula_List_Access;
      end record;

   type Formula_List_Access is access Formula_List_Type;

private

   type Symbol_Type is new Integer;

end Formulas;

Note that we can choose either Formula_Type or Formula_List_Type as the primary type for representing formulas. (E.g. 2+2 operation could be either operation(2(), +, 2()) or (2(), +, 2()). I introduced special symbol operation to be the top level head of all formulas.) I don't see any principal reasons to choose either of two. What is better?

Your participation

You are welcomed to participate in the development of this software. You can use CVS at SourceForge project page or send patches and program fragments. Also you can use this Wiki collaboration area.

You are expected to know Ada95, however the decision to write it namely in Ada is not yet 100% final.

Please email me if you want to take part.

Current Development Plans

Today the method itself is not yet developed in details.

However the are already certain things to code now:

concept and implementation of modularity and local symbols (analogous to local variables and modules/packages in conventional programming languages);
representing 21MM data structures in Ada95 (It should use copy on write reference counting for expressions and subexpressions);
parser and formatting for the lisp-like notation of 21MM:
- we may split it into tokens where '(' and ')' are tokens, alphanumerics and '_' form tokens, and all other characters also form tokens. E.g. (2e+-a_b) would be 5 tokens: (, 2e, +-, a_b, ). Tokens can also be whitespace-separated.
matching and co-matching related routines;
persistence of data in a binary format;
XML export and import;
integration with C and Ada95 API;
integration with Readline library;
integrating library support of long integers (it is possible to code in 21MM itself but that would be slow) and probably some other otherwise slow mathematical functionality;
managing (potentially big) in-memory database of formulas with different views optimized for accessing different kinds of objects; quick enumerating expressions (co)matching a pattern; possibly caching of formulas for faster access;
GNU compatible .tar.gz package structure, Debian Linux package support, Windows installer.
test suite randomly generating theorem proofs and searching for a contradiction.

References

My homepage | My math page | My math news | Donate for the research