I would also suggest that this effort seriously consider using COLORE as a container for the preliminary work. Aside from a desire to go on to identify a set of ontological primitives, I am having difficulty distinguishing the idea of the respository as sketched out on this list from that of COLORE.
You can add OpenCyc to it if you like, and define a metalevel relation that indicates that it is somehow "foundational." COLORE on its own doesn't enforce such rigidity, rather allowing users to identify how ontologies in the repository relate / map to one another. You can then utilize / order these mappings in whatever way you see fit, i.e. perhaps by enforcing an ontological primitive hierarchy.
Otherwise, perhaps consider using IKL as the representation language, which would definitely differentiate the work, but you can also still reuse a lot of what's in and will be going into COLORE. To my mind, it doesn't make much sense to duplicate work, unless of course i'm missing something really important here :D.
Also, my note below isn't meant to suggest that descriptions in Common Logic or whatever formalism _captures entirely_ whatever it is we're representing in a formal ontology. Simply, that if we want to use computers effectively to aid whatever problems we're using formal ontologies for, it is important to consider the language of representation and to utilize whatever built-in advantages it may offer us to their maximum potential. One can always add natural language (or even higher order logic) elaborations of their domain. Their use for computers at the moment is limited, but of course it greatly aids designers and the humans who uses these software artifacts.
Lastly, the idea of logical "primitives" isn't really new, though it hasn't quite been articulated or implemented in the way I sketched out below. Description Logics implicitly use the same idea, when providing black box relations such as "Transitive" or "Symmetric" etc., for knowledge engineers to use. Aside from the ability to write your own "logical primitives" that arises from the move to Common Logic or FOL, structuring these primitives intelligently in a repository also enables the development of a number of pretty useful tools and applications (i.e. axiom generation, semantic mapping, ontology alignment, etc.).
Cheers,
Ali
On Fri, Feb 19, 2010 at 4:18 AM, Ali Hashemi <ali.hashemi+ontolog@xxxxxxxxxxx> wrote:
Dear Ontolog,
The discussion on growing a family of interlingua ontologies in a repository is very stimulating.
I would suggest the following things need to be considered:
==================================
1) What is the granularity of a module that one would wish to allow? A single statement in logic is ostensibly a theory, and can be considered a module. However, this leads to an exponential proliferation of modules. Any repository should have some guidelines as to what constitutes a module.
==================================
2) Allowing and capturing all different (but logically equivalent) axiomatizations of an intuition is laudable goal, but it introduces serious problems in terms of _possibly_ exponential growth for the repository (i.e. maintain several parallel modules and hence lattice of theories). But more importantly, it is also nightmare in terms of updating, maintaining and growing the repository. It can be done, but it is not a trivial task, and would need very clear guidelines for how the repository would handle updates / changes to any particular module. Moreover, how might one handle the extension of one module? There are several possible solutions, but each have their drawbacks.
I realize i'm a pretty abstract person, so i'll ground this in an example.
There are at least two ways of characterizing the notion of a lattice. One can do it with the "less than or equal" relation, or one can use the functions of meet and join. Both result in a set of isomorphic models. Let us assume that the repository contains both characterizations of this intuition. Now say I decide to extend the module for lattice based on meet-join. Should I also create a parallel entry for this extension based on leq? Perhaps one might respond -- well, whichever axiomatization people use is the one we need to worry about, if someone wants to extend the alternate description, they can create a parallel entry.... This is certainly one approach, but I believe it introduces serious concerns for maintaining and updating the repository.
==================================
3) I humbly suggest there are two ways one can construct "upper ontologies" -- one is to focus on things as they are in the real world (the traditional upper ontology approach), and the other is to focus on the language one is using to describe said things. Both approaches provide significant advantages for reuse, but ignoring one introduces significant hurdles. I seem to have been unsuccessful thus far in communicating this idea, but will try once more:
The infinite lattice of theories can take on various guises. The most straightforward application involves an ontological stance, where one describes things such as "spatio temporal thing", and specializes from there by adding axioms. Refer the diagram below for how adding axioms / extending theories results in a corresponding tightening of what I term "model spaces." In the diagram below, arrows pointing right constitute "non-conservative extensions" of a module (think of the lattice of theories turned sideways, where down is now right). The "model space" below is the set of permissible models (in the Tarski sense) that are allowed by the axioms. The more general modules (i.e. less axioms) permit more models, and each non-conservative extension "slices up" the model space of the more general theory.
A complementary lattice of theories which doesn't fit neatly into the above is a fundamentally more abstract, but just as useful exposition of descriptions in the language. Instead of focusing on the pragmatics, it exploits the semantics of the theory, specifically the relationship between axioms and the set of allowable models (Tarski sense).
As an example, let us consider a common characterization of time as branching points. For the sake of brevity, let's assume time is discrete moments, (it really doesn't matter for our purposes here). While the pragmatics of our axioms might connect the symbols
(forall (t1 t2 t3)
(if (and (before t1 t2) (before t2 t3))
(before t1 t3))
*t1, t2, t3* are time points or moments, and *before* captures an intuition for how time points relate to one another, a common analogy to help conceptualize this is of course, literally branching time...
The above is also quite clearly a classic application of the axioms for transitivity applied to the notion of ordered time points. Quite aside from the above axiom being the specialization of some concept of time, it is also a specialization of the logical structures that arise from describing time in a language such as first order logic. In a way, there are two sorts of "primitives' (i use this term very loosely) here. One is the "primitive" notion of timepoint, or perhaps more generally, time. The other is the "primitive" notion of ordering, or specifically for branching time, partial ordering.
i.e. one can remain agnostic on ontological commitments, and simply flesh out the logical implications of the statements. Obviously, this approach on it's own is useless, since in the end we need to connect our theories to the real world, but it would be a serious oversight to not consider and incorporate this perspective in the construction of any "foundation ontologies."
More specifically, if in the construction of any such repository, we keep track of both extensions (ontological and logical), we would be able to greatly ameliorate the task of generating semantic mappings and hence interoperability. (If you would like more details on how this might work, a bit outdated but perhaps still useful exposition on this idea can be found in my Master's thesis.)
==================================
I'll end here for now. I have much more to add, but this email is already quite long and I imagine some of these issues might be touched upon in this morning's conference call.
I would also suggest that those interested in the types of mappings available when one uses Common Logic to check out the forthcoming FOIS 2010 proceedings. There will be a paper there that will quite rigorously spell out many (though not all) of the possible connections / mappings between theories (both ontologically and logically). It would probably save a lot of effort in terms of reinventing wheels and should help clarify many of the issues that undertaking the creation of such a repository will entail.
Best,
Ali
--
(•`'·.¸(`'·.¸(•)¸.·'´)¸.·'´•) .,.,
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (01)
|