|
To extend Chris' points a bit as well, I'd like to take this opportunity to clarify a few notions. The text below is directly related to the conversation I've been having mainly with Matthew West in the 3D-4D thread, some of the questions that Rich McCullough has recently alluded to and the email which started this thread.
I've noticed that on this forum, there might not be a clear understanding of what a logical (Tarski) model is, how exactly such models are connected to the underlying axioms and perhaps most importantly, why one should care (how the relation may be usefully exploited).
Similarly, I'm not sure the value of representation theorems and the different possible types of mappings are well appreciated. I apologize in advance if all this stuff is obvious, but it's useful to get it out and perhaps to eventually migrate this discussion to the wiki after some criticism / feedback.
----- *Models* The following is but a brief overview of what models in the logic sense are. Wiki ( http://en.wikipedia.org/wiki/Model_theory#First-order_logic and http://en.wikipedia.org/wiki/First-order_logic#Models ) has two decent entries, though numerous well written texts abound on the matter.
Models are created via a particular interpretation of the axioms.
Axioms, aside from the logical operators, essentially consist of relations and variables. An interpretation assigns particular objects in the domain of discourse to the functions, relations and constants/variables.
So imagine i have a relation called "supervises" which might look like:
(forall (employee1 employee2) (supervises employee1 employee2) <-> [some axioms...] The extension of supervises is the set of all employee pairs for which the relation holds true. Any subset of these tuples is a valid model for "supervises." These pairs constitute a model of supervises. Now why is logic useful here? How is this differentiated from a simple taxonomy? If we stay within the bounds of first order logic (or even common logic), we may make use of Soundness and Completeness to know that the truth values of our models are preserved are always preserved regardless of how the axioms are interpreted.
Specifically, let Th(P) be a theory (a set of axioms). Then there is associated with it, a set of models M(P). Each of these models satisfies the axioms of Th(P). Moreover, anyone interpreting Th(P) is guaranteed to generate models, or verify models which are a subset (or all of) of M(P). Anyone else, coming along and looking at these axioms will always be talking about the same set of models. This is what soundness and completeness guarantee us.
Contrast this with natural language or really any representation which is underspecified / lacks adequate axioms. In such a context, the link between the assertions of the representations, and models which satisfy those assertions is not as clear. Imagine I have a language which only defines "space" or "time" as a name. If no axioms are given to specify which sense, or possible interpretations are appropriate / applicable, then there is no guarantee that two people are talking about the same thing.
Thus, were I to assert X @(space x y z)&(time t), it would be unclear what I mean by each of those terms. Looking at time: is it a linear ordering of points? is it a branching of points? is it a set of intervals? etc.
Depending on which sense of time I pick, it will radically alter the models I can construct from such a statement.
Each variation leads to different sets of models. Thus, without adequate axioms, I cannot guarantee that someone else, coming along, would produce the same intended models that i had wanted. It is next to impossible for me to share my work with you using only what I have explicitly stated, since the models i was intending by using "time" may be different from yours. The only way to enforce that what i intended is what is reproduced, would be to include axioms or to include such sense disambiguation at the metalevel. If such material is included at the metalevel for human consumption only, that is fine, but then we're missing the point of machine readable knowledge and ontologies on computers.
This is one reason axioms are important. It pushes the semantics - what i intend to mean - right down to the level of what is explicitly stated; ideally to the maximum extent possible in a machine readable form. Such a representation enables querying, automated reasoning, automatic model generation, model satisfaction tests etc.
Another, important way the utility of axioms is motivated can be seen by considering the different types of equivalences (even partial) it then enables. This is the bread and butter of true semantic interoperability.
*Representation Theorems* This section shows (very briefly) how the concept of a Representation Theorem in math may be extended for use in ontologies. We recall that fundamentally, formal logics tell us how to connect abstract symbols or "objects" to things in the real world. Axioms aren't saying anything directly about the world. As a form of media (yes, language is a medium!), they are simply asserting how various symbols are connected to one anohter. It is the interpretation which connects the assertions to actual things in the world.
At first glance, this might seem like a drawback, yet in fact, this is one area where the utility of formal logics come to shine. Let's consider supervises again. Imagine we are wish to assert that in a company, every employee is supervised by another employee, except for the CEO. And if A is supervising B, and B supervises C, then in a sense, A is also supervising C. Such an assertion restricts the types of acceptable models. Specifically, it restricts "supervises" to models which resemble company organization charts -- one person at the top branching downwards, with accountability flowing upwards, eventually leading to the CEO.
*Logical "Structures"* Now if, we strip the model for supervises of its links to the domain, all we have left are a set of abstract objects connected to one another in a particular way. Say empty boxes and lines connecting them - basically a company organization chart, but you aren't mapping "lines" to "supervises" nor "boxes" to "people" (or positions).
This resultant object, is what I call a "logical structure." It's the structure of a particular model (or ideally, a class or category of models), devoid of an interpretation.
What is great, is that these logic structures are reused in diverse fields to capture the behaviour of highly differing objects. In fact, the supervises relation above has a logical structure that is isomorphic to that of bounded join semi lattices (BJSL). Specifically, the axioms may as well have been written using less than or equals to, and any abstract objects x and y: (leq x y) <-> [bounded join semi lattice axioms]. That is to say, we could use the axioms for BJSL with an interpretation that connects supervises to leq, x to employee1 and y to employee2. Moreover, if we can show that for any (all) models of axiom_set1, Th(P), the resultant models of axiom_set2, Th(Q) preserve the same truth structures, we have proven a Representation Theorem.
This means that the structures of Th(P) are captured by models of Th(Q). And more importantly, that the target category of supervises can be replaced by other well understood categories - in this case, partial orders. We have reduced the problem to one that we might better understand.
We make use of this all the time in math, and informally, in natural language - indeed, this is what a conceptual / structural metaphor is! It is mapping the logical substructures that we use to make sense of one concept area, to another concept; hence the bohr description of the atom shares structural similarities (how objects in the theory "connect" to other objects) with that of the solar system.
Now as others have also pointed out, we don't always establish full mapping from Th(P) to Th(Q), we may prove a representation theorem only for a particular subset of those axioms, or even for a single relation (though we would rarely call this a representation theorem). Regardless, what we are saying in a representation theorem is "these class of models are describable by these other class of models."
One particular application of this insight about logical structures, is that we might even begin defining concepts in such a way, but this is a digression here (i.e. the ontology design algorithm i've alluded to in previous posts).
On track - Representation Theorems correspond to the one of the strongest forms of linking between two sets of axioms. A related concept is that of Relative Definability. Semi-formally, we say that A is Definably Interpretable in B, if we may define every concept in A using only concepts from B. See (Bennet 2004) for a full exposition of this topic.
There are weaker forms of connecting a theory to another. One way might be to show that two theories are mutually consistent given a particular mapping axiom - indeed, an algorithm has been developed which does exactly this.
*Axioms!* Axioms are not intended to replace natural language. The two forms aren't really competing with one another since they serve different but complementary purposes. The primary utility of axiomatization is in the precision and reproducibility it affords due to Soundness and Completeness. Second, it enables us to better leverage what computers are good at. Thirdly, we can then exploit these representations to either implement algorithms or to complement less expressive but more tractable representations.
Thus, while there is tremendously utility in classification schema, and while description logics capture large fragments of First Order Logic (FOL) having been be selected to be computable, it certainly helps to have axioms. Axioms reduce ambiguity and enable the generation of all types of useful semantic mappings fairly directly. No need for lexical matching.
Moreover, the the addition of axioms aren't to replace what has been done. Rather, they complement (relatively) opaque taxonomies, by extending and clarifying the different senses of what the terms mean. One need not even do the actual implementation in full FOL or Common Logic, restricting computation to only fragments of such theories (perhaps captured in OWL or RDFS). Though a case may be made today that contemporary computing tools make CL ontologies feasible, computational implementations.
Regardless of the implementation choice, having axioms written for concepts in a formalism such as Common Logic greatly enhances the prospects for interoperability - even the natural language kind. For example, if a biologist notices that the logical structures for "membrane permeability" and "diffusion" are remarkably similar to those for "resistivity" and "current" in electronics, it might put people from erstwhile disparate domains in touch with one another. Might there be other similarities between the two fields that have been hitherto overlooked? Particularly, such mappings greatly alleviate the problem of wheel reinvention we are faced with when names become more important than structures resulting in the obfuscation of links which exist among superficially "silo'd" domains.
---- Hope the above wasn't too pedantic and communicates to readers on this list both what is meant by some of the terminology used in more formal ontologies and how they are applicable to real world problems.
Cheers, Ali On Sun, Mar 15, 2009 at 7:55 PM, Christopher Menzel <cmenzel@xxxxxxxx> wrote:
-- (•`'·.¸(`'·.¸(•)¸.·'´)¸.·'´•) .,.,
_________________________________________________________________ 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) |
