Nicolas,
One footnote I should mention to be more precise - when I mention
proving the consistency of logical theories, I'm only talking about
exploring the space of possible inconsistencies, since one can't guarantee
the consistency of an arbitrary first order theory, one can only perform an
incomplete search for inconsistencies. However one can I think have
reasonable confidence about the absence of an inconsistency affecting
practical inference for a given theory, given a modern theorem prover and
sufficient computing resources. (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)
|