[Attempto] nonstructural restrictions on Owl 2 axioms and AceWiki

[Kenneth Jones]

Hi Tobias,

In prior emails we have discussed the Nonstructural Restrictions on Owl 2
Axioms<http://www.w3.org/TR/2008/WD-owl2-syntax-20080411/#Nonstructural_Restrictions_on_Axioms>and
their implications for AceWiki.  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.

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.

I googled and found a discussion of this issue at
http://www.nabble.com/Property-chain-conflicts-with-cardinality-constraints-td18705930.html.
This article mentions a Pellet option, Pellet species detection, and some
work at Manchester that may be useful.  You may be able to test how each
sentence affects the ontology before submitting it to Pellet.  (Of course,
if the available tools don't work incrementally then this could be a giant
performance hit for large ontologies.)  If the sentence would make the
ontology Owl-Full then the sentence could be marked with a red triangle and
it could be excluded from reasoning.  If you take this route you could lift
the total ban on sentences that explicitly define transitive properties and
flag only the problematic ones.  Eventually you might even consider adding a
full-blown theorem prover to AceWiki.  When a user enters a sentence with a
translation that violates the nonstructural restrictions you could give the
user the option to excluded the sentence from reasoning or to switch to the
theorem prover.  Of course, you would have to display a dialog box that
explains the trade-offs in terms the user could understand.

Simplicity is of paramount importance in AceWiki and I'm sure you consider
the correctness of inferences to be equally important.  The challenge will
be to come up with a solution that makes correct inferences, is sufficiently
fast, and is very simple from the point of view of the user.

It's times like this that make me wonder if decidability is highly
overrated! :-)

-- Ken
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20081026/4fcbb34c/attachment.htm