RE: LC Comment: "Hidden" Axioms

-----Original Message-----
From: Bijan Parsia [mailto:bparsia@cs.manchester.ac.uk] 
Sent: Friday, January 23, 2009 4:58 PM
To: Solbrig, Harold R.
Cc: W3C OWL Working Group
Subject: Re: LC Comment: "Hidden" Axioms

On 23 Jan 2009, at 22:46, Solbrig, Harold R. wrote:

[snip]

>> Let me mention related requirement that we have encountered.  We  
>> have a
>> need to be able to classify an ontology and subsequently transmit
both
>> the asserted and the logical inferences for display and consumption
in
>> secondary resources such as wikis and other tools.  As these tools
may
>> create additional axioms, we need to differentiate the asserted from

>> the
>> inferred - both as important information to the editors and to be
able
>> to remove or ignore these axioms when the modified ontology is
>> subsequently re-classified. While this is a slightly different use  
>> case,
>> it still involves the same notion - some sort of tag or property on
an
>> axiom that affects the way that it is interpreted.

> Actually, from a logical point of view the added inferred axioms are  
> harmless...they were already "in" the annotation. So a simple  
> annotation which indicates that it was inferred would be fine ---  
> editors could not display them, or try to verify them, but if some  
> tool passed it to a reasoner...the reasoner would just have an easier

> time :)

True only if the editors didn't add (or remove) one or more non-inferred
axioms.  Then, it would be important to strip the inferred axioms before
re-classifying.  Obviously, this could be done pre-reasoner as long as
the inferred tag was available.  

> (Of course, if you were trying to *test* the reasoner...putting in the

> entailments from some other reasoner wouldn't be good. So there's  
> still some justification there. I just think it's somewhat less
severe.)

Interesting point. The "inferred" tag would allow you to combine the
input and result of a test cases into a single source.  Instead of an
input and result, just a one set of defined and inferred axioms.  

Cheers,

Harold Solbrig

Received on Friday, 23 January 2009 23:12:05 UTC