[Attempto] nonstructural restrictions on Owl 2 axioms and AceWiki

[Kaarel Kaljurand]

Hi,

On Sun, Oct 26, 2008 at 4:20 PM, Kenneth Jones <kennethjone at gmail.com> wrote:
>
> In prior emails we have discussed the Nonstructural Restrictions on Owl 2
> Axioms and their implications for AceWiki.

The latest version of these restrictions (which are now called "global
restrictions") is

http://www.w3.org/TR/owl2-syntax/#Global_Restrictions_on_Axioms

In this version, there are also more examples than in earlier versions.


> You have eliminated one possible
> violation of these restrictions by excluding the explicit definition of
> transitive properties from reasoning and displaying red triangles preceding
> the sentences that define them.
>
> It occurred to me that I could use the following set of sentences to make a
> cardinality-restricted property transitive, without actually declaring the
> property to be a transitive property:
>
> If X immediately precedes Y then X precedes Y.
> If X immediately precedes Y and Y precedes Z then X precedes Z.
> If X precedes Y then X is a sequence element.
> If X precedes Y then Y is a sequence element.
> Every sequence element is immediately preceded by at most 1 sequence
> element.
>
> Where, of course, I have defined the noun "sequence element" and the verbs
> "precedes" and "immediately precedes".
>
> AceWiki accepted all of these sentences and loaded them into Pellet.  I
> created the seven proper names "Element 1" through "Element 7" and I linked
> them with the "immediately precedes" verb.  The queries "What precedes
> Element 1?", "What precedes Element 4?", "What precedes Element 7?", and
> "What is a sequence element?" were all answered correctly.  I defined the
> proper name "Element 2-2" and tried to enter the sentence "Element 2-2
> immediately precedes Element 3" and the sentence was recognized as
> inconsistent with the existing sentences and was displayed in red.  So all
> my tests (queries) passed and everything looked great.

As far as I can tell, the second sentence is not needed for these
inferences to hold.
So if Pellet just ignores the second sentence (because it is in
violation with the global
restrictions), then you still get the correct inferences. Only the
inferences that require
the second sentence to be present won't show up.


> Of course, I realized that I must have violating the Nonstructural
> Restrictions even though I hadn't created a sentence that was translated
> into an Owl statement that contained TransitiveObjectProperty(precedes).  So
> I'm worried that it might be possible for a user to unwittingly violate the
> Nonstructural Restrictions, think everything is fine, and have Pellet go
> haywire at a later time when just the right combination of axioms has been
> defined.

Yes, just disabling transitive properties syntactically will not work
in general.
It would provide a better solution if OWL API could be queried to find out
if the ontology violates these restrictions. It wouldn't make sense to
implement this checking in AceWiki as OWL reasoners and OWL APIs will have to
provide it anyway.

--
kaarel