Re: SUO: Re: SUMO axiomatization
Thanks, John. Also, I mentioned in a context about ontology integration,
that these (IMPS) used the notion of "little theories" and theory
interpretation to interrelate/map theories. Obviously a possibility for
SUO (and maybe via IFF).
Leo
"John F. Sowa" wrote:
>
> 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
--
_____________________________________________
Dr. Leo Obrst The MITRE Corporation
mailto:lobrst@mitre.org Intelligent Information Management/Exploitation
Voice: 703-883-6770 7515 Colshire Drive, M/S W640
Fax: 703-883-1379 McLean, VA 22102-7508, USA