Nicolas,
Proving the consistency of an ontology, or portion of an ontology is
both an essential step in the process of formal ontology development, and a
selling point for formal ontology itself. Most OWL ontologies have very
limited formal content that allows for automated checking, such as
class-subclass, argument typing and cardinality. A formal ontology with
rules allows for a more complete definition of terms, and therefore
supplies more content that can be checked automatically with a theorem prover. (01)
Adam (02)
At 10:50 AM 12/10/2004, Nicolas F Rouquette wrote:
>Has anybody noticed a strong kindship between the issues we face in
>modular / formal ontology development
>relative to issues of mapping and the ideas of Galois connections &
>"theorems for free" ?
>
>While I was listening to Mark Musen's presentation,
>
>http://ontolog.cim3.net/cgi-bin/wiki.pl/wiki.pl?ConferenceCall_2004_12_09
>
>I started to think about how good software engineering practices solve
>some of the
>problems of ontology development such as those Mark mentioned in the context
>of NCI's change management process.
>
>The issues there are about dealing with the distributed changes to various
>parts
>of an ontology or to several ontologies that are used in diverse combinations.
>The problems stem from the fact that we can never anticipate all possible
>ways in which somone is going to use an ontology or depend on several
>ontologies.
>The changes made can affect such users and break the logical foundations they
>need for whatever reasoning tasks they do (classification, subsumption,
>query, optimization, compilation, ...)
>
> From a software point of view, it seems that ontology development lacks
>a precise way to talk about software engineering notions like scope, contract,
>dependencies, extension points, .... I know that there's a lot of work in
>ontology
>with the notion of "topic map" and "concept map"; I don't know enough about
>that line of work to tell if the issues they have looked into adress all
>of the
>software engineering concerns of distributed change management.
>
>There is an alternative approach to change management with the idea
>of using category theory, Galois connections and theorems for free as
>a heavy-duty machinery to "proove" that the consequences of changes
>made in an ontology wouldn't break properties we need in uses of that
>ontology.
>
>This alternative approach is based on a paper I read from Kevin and Roland
>Backhouse:
>
>http://portal.acm.org/citation.cfm?id=1007979
>
>Kevin and Roland show an application of theorems for free and Galois
>connections
>in order to "proove" statements (safe abstract interpretations)
>about a set of things (implementation level) in terms of logical
>properties about
>functions and the way they are used to build an implementation (this is
>where I understand
>we need to have a parametric and higher-order capability to talk about
>functions and about their application)
>
>I wish that I could fully understand Kevin and Roland's paper.
>Alas, I was raised in France, not Britain; but the more I attempt
>to understand their paper, the greener British grass looks to me.
>
>Seriously though, we can take a step back and see:
>
>- OWL made a number of tradeoffs biased towards practicality.
>- the field of abstract interpretation, etc... offers a number of
>interesting ways
> to get help from formal specifications
>- an ontology is a formal specification of some kind
>
>The connection here seems to me that:
>
>- the DL formulas we use in an ontology stand for the functions that Kevin
>and Roland use to talk about abstract specifications
>
>(e.g the x operator introduced in their running example on p. 2)
>
>- the "fold" function stands for a specific kind of logical inference like
>classification, subsumption, etc..
>
>(e.g., the concept of "defined class" in Protege/OWL)
>
>Is this just a French/British cultural joke or is there something worth
>pursuing here?
>
>My hunch is that theorems-for-free says: "here's a way to put a theorem
>proover to a practical use for ontology
>development to answer some practical questions in a different way than is
>currently done or not done at all,
>e.g.: upper/lower ontology consistency; compatibility of multiple upper
>ontology mixins.
>
>
>If these comments make sense to you, I'd be very interested to read your
>opinions/feedback/suggestions about them.
>
>-- Nicolas.
>
>_________________________________________________________________
>Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
>Subscribe/Unsubscribe/Config:
>http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
>Shared Files: http://ontolog.cim3.net/file/
>Community Wiki: http://ontolog.cim3.net/wiki/ To Post:
>mailto:ontolog-forum@xxxxxxxxxxxxxxxx (03)
----------------------------
Adam Pease
http://www.ontologyportal.org - Free ontologies and tools (04)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Unsubscribe/Config:
http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (05)
|