[Top] [All Lists]

Re: [ontolog-forum] Ontology mapping & "theorems for free"

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>, ontolog-forum@xxxxxxxxxxxxxxxx
From: Adam Pease <adampease@xxxxxxxxxxxxx>
Date: Fri, 10 Dec 2004 10:54:35 -0800
Message-id: <>
   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,
>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 
>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 
>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 
>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 
>This alternative approach is based on a paper I read from Kevin and Roland 
>Kevin and Roland show an application of theorems for free and Galois 
>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/
>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/
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (05)

<Prev in Thread] Current Thread [Next in Thread>