SUO: Re: SUMO axiomatization
There is a collection of over a hundred mathematical theories
(fully axiomatized) that were developed to run under IMPS
(Interactive Mathematical Proof System). The theorem-proving
programs that use these axioms run on most versions of LISP and
are available from Mitre as software that has been made freely
available. Following is the home page:
http://imps.mcmaster.ca/
The theories include graphs, groups, fields, automata,
and several versions of geometry, arithmetic, etc.
MITRE has granted a public license for use of this material.
Following is the first paragraph:
The MITRE Corporation (MITRE) provides this software to you without
charge to use, copy, modify or enhance for any legitimate purpose
provided you reproduce MITRE's copyright notice in any copy or
derivative work of this software.
See the following file for the full license:
http://imps.mcmaster.ca/imps-system/public-license
Since MITRE has put very few restrictions on their license, they
would probably be amenable to making the software and axioms
available to the IEEE with any license modifications that the
IEEE might require.
Suggestion: Rather than develop a new collection of mathematical
axioms for the SUO, which may or may not be consistent with IMPS,
I recommend that the SUO adopt the IMPS axioms from MITRE as the
basis for the mathematical modules in SUMO and other SUO projects.
Following are the reasons:
1. The IMPS axioms have been under development since 1990 and have
been tested in theorem-proving programs that have been used at
many universities and research institutions. That gives some
assurance that most, if not all, of the major bugs and problems
have been recognized and corrected.
2. The IMPS notation is based on a typed predicate calculus written
in a LISP-based notation, which should be fairly easy to translate
to KIF and other related versions of logic, such as CGs.
3. There is extensive documentation available on the IMPS web site,
including about two dozen published papers and technical reports.
Folllowing is the user's manual:
http://imps.mcmaster.ca/manual/
Following are the more theoretical papers:
http://imps.mcmaster.ca/doc/major-imps-papers.html
John Sowa