Alex,

Thanks for that info.   Zalta's Principia is a huge compendium (1501 pages with more to come) of formal definitions and proofs.  The Isabelle theorem prover is an excellent basis for automated reasoning with and about anything that uses those definitions.  And the supporting software can be downloaded for free.

As I said before, I was highly skeptical about any formal definitions developed in Ontolog Forum, because this is not a standards organization.  However, if the definitions are taken from or based on Zalta's Principia and supported by Isabelle, they can be posted in web pages shared by anybody and everybody.   I'm sure that Stanford would support or collaborate with anybody who develops such a repository.

Re Top-Level Ontologies:  The TLOs are specified in very restricted formats in a tiny subset of first-order logic.  Isabelle supports all of FOL plus much, much more.  As I have been pointing out, FOL is much simpler, more general, easier to use, and faster than OWL2.  The availability of Isabelle with all of the definitions in Zalta's tome would make a strong argument for OWL3 (the same notation for the hierarchy as OWL2, but full FOL as an upgrade).

There is a question about Common Logic, which is a different extension to FOL,  I believe that the HeTS tools could be extended to support mappings of CL to and from Isabelle. There are various issues about the mappings, and HeTS is sufficiently general that it could be extended to support them. 

Any TLO specified in OWL can be automatically mapped to FOL (the extension to OWL3) and used with anything specified in the Zalta's system.   Although Isabelle supports HOL, a large majority of the structures defined by Zalta use only the FOL subset.

Common Logic is a different extension to FOL.  The HeTS tools  and the OMG standard for DOL could be used to do the mappings. 

Since Isabelle also supports FOL as a subset, it would be a good tool for supporting OWL3.    That's another argument for getting rid of the limitations and exceptions of OWL2 and move to OWL3.  Existing applications that use OWL2 would not be affected.  But new applications could use the simpler OWL3 notation.

For more about Isabelle and links to resources, see the Wikipedia page:  https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) .

John

_______________________________________