- From: Birte Glimm <bglimm@cs.man.ac.uk>
- Date: Thu, 5 Nov 2009 17:39:54 +0000
- To: Wael Yehia <wmyehia2001@yahoo.com>
- Cc: public-owl-dev@w3.org
- Message-ID: <492f2b0b0911050939p41f073adj350c4cdf56855403@mail.gmail.com>
2009/11/5 Wael Yehia <wmyehia2001@yahoo.com>
> Hello everyone,
> I'm trying to use some reasoner that supports OWL 2, fully, and I'm
> particularly interested in being able to reason with the Universal Role
> (represented by the topObjectProperty), the role that relates every pair of
> individuals in the domain.
> Now, I noticed that Protege 4.0 does not have a keyword for
> topObjectProperty or at least it is not predefined and appear at the root of
> the property hierarchy, the way the Thing (top) concept is predefined and is
> at the root of the concept hierarchy. Maybe because protege 4.0 doesn't
> support OWL 2 fully yet.
Protege 4.0 is not really OWL 2 ready. You would need Protege 4.1, which is
not yet officially released. We just released HermiT 1.1 and from the HermiT
website, you can also get a compiled version of Protege 4.1 (no support and
no guarantee that it is working, it is not an official Protege release).
> And creating a new property with the 'topObjectProperty' name won't make it
> the topObjectProperty that we need but just some another property, because
> by looking at the rdf output when you save the ontology you'll see that the
> topObjectProperty that you defined is prefixed with your ontology's name and
> not the 'owl:' prefix which is presumably the right one.
>
Yes, without the owl prefix it is not really the top property.
> I wrote some test cases manually, this is one of them in First Order Logic
> (FOL):
> (\forall x.F(x)) \and \not (\exist x.F(x))
>
That can directly be expressed as a DL axiom:
SubClassOf(owl:Thing :F)
SubClassOf(owl:Thing ObjectComplementOf(:F))
in other syntax
top implies F
top implies not F
(I used two axioms because in your example the two x are not really the
same, you could rename one into y due to the quantifier scope)
> which is equal to: \forall x.False
>
not equal, but it follows
> I am not sure if this formula is satisfiable, maybe if the domain is empty.
>
The domain is required to be non-empty, so it is unsatisfiable.
> But it can be translated to Description Logic (DL) using the Universal Role
> (topObjectProperty) and becomes
> \forall U. Bot
> or in manchester syntax:
> topObjectProperty only Nothing
>
No need for the top role, as said above. All axioms apply to all
individuals, they can be seen as usiversally quantified.
If you use the top object property, your domain can still have one element,
but that element cannot have a successor. The ontology is still satisfiable
though.
> Now, my concern is that I'm not 100% sure that I'm expressing the formula
> in RDF syntax (which i will show below) correctly, and therefore don't know
> how Hermit 1.0 (which claims that it supports OWL 2) is understanding it.
HermiT understands what you say, but you probably don't want to use the top
object property.
> So, if anyone knows whether this is correct syntax, or knows anything about
> Hermit's reasoning capabilities with topObjectProperty, then any advice or
> hints are greatly appreciated.
HermiT supports indeed all of OWL 2 including owl:topObjectProperty.
> This is my RDF syntax ontology, I don't know if I should include parts of
> it here or all of it, so I decide to put it all here, and please note that I
> cheated a bit and used protege to output it for me and then i manually
> changed the occurrences of topobjectproperty with two version of my own:
> 1) #TopObjectProperty .... I tried this one because protege shows it as
> a super property of any new property you create so I thought maybe it
> recognizes it this way
> 2) owl:topObjectProperty
>
> only the second one is the top object property. The first one is just a
normal property for HermiT.
> This is the RDF ontology:
>
>
> <?xml version="1.0"?>
> <!DOCTYPE rdf:RDF [
> <!ENTITY owl2 "owl:" >
> <!ENTITY owl "http://www.w3.org/2002/07/owl#" >
> <!ENTITY xsd "http://www.w3.org/2001/XMLSchema#" >
> <!ENTITY owl2xml "http://www.w3.org/2006/12/owl2-xml#" >
> <!ENTITY rdfs "http://www.w3.org/2000/01/rdf-schema#" >
> <!ENTITY rdf "http://www.w3..org/1999/02/22-rdf-syntax-ns#<http://www.w3.org/1999/02/22-rdf-syntax-ns#>"
> >
> <!ENTITY O3 "http://www.semanticweb.org/ontologies/2009/9/O3.owl#" >
> ]>
> <rdf:RDF xmlns="http://www.semanticweb.org/ontologies/2009/9/O3.owl#"
> xml:base="http://www.semanticweb.org/ontologies/2009/9/O3.owl"
> xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
> xmlns:owl2xml="http://www.w3.org/2006/12/owl2-xml#"
> xmlns:owl="http://www.w3.org/2002/07/owl#"
> xmlns:xsd="http://www.w3.org/2001/XMLSchema#"
> xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
> xmlns:owl2="owl:"
> xmlns:O3="http://www.semanticweb.org/ontologies/2009/9/O3.owl#">
> <owl:Ontology rdf:about=""/>
>
> <!--
>
> ///////////////////////////////////////////////////////////////////////////////////////
> //
> // Object Properties
> //
>
> ///////////////////////////////////////////////////////////////////////////////////////
> -->
>
> <!--
> http://www.semanticweb.org/ontologies/2009/9/O3.owl#TopObjectProperty -->
> <owl:ObjectProperty rdf:about="#TopObjectProperty"/>
>
> <!-- owl:topObjectProperty -->
> <owl:ObjectProperty rdf:about="owl:topObjectProperty"/>
>
> <!--
>
> ///////////////////////////////////////////////////////////////////////////////////////
> //
> // Classes
> //
>
> ///////////////////////////////////////////////////////////////////////////////////////
> -->
>
> <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#A -->
> <owl:Class rdf:about="#A"/>
>
> <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#Last -->
> <owl:Class rdf:about="#Last">
> <owl:equivalentClass>
> <owl:Class>
> <owl:intersectionOf rdf:parseType="Collection">
> <owl:Class>
> <owl:complementOf>
> <owl:Restriction>
> <owl:onProperty
> rdf:resource="#TopObjectProperty"/>
> <owl:someValuesFrom rdf:resource="#b"/>
> </owl:Restriction>
> </owl:complementOf>
> </owl:Class>
> <owl:Restriction>
> <owl:onProperty rdf:resource="#TopObjectProperty"/>
> <owl:allValuesFrom rdf:resource="#b"/>
> </owl:Restriction>
> </owl:intersectionOf>
> </owl:Class>
> </owl:equivalentClass>
> </owl:Class>
>
>
>
> <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#b -->
>
> <owl:Class rdf:about="#b">
> <owl:equivalentClass>
> <owl:Class>
> <owl:intersectionOf rdf:parseType="Collection">
> <rdf:Description rdf:about="#A"/>
> <rdf:Description rdf:about="&owl;Thing"/>
> </owl:intersectionOf>
> </owl:Class>
> </owl:equivalentClass>
> </owl:Class>
>
>
>
> <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#c -->
>
> <owl:Class rdf:about="#c">
> <owl:equivalentClass>
> <owl:Class>
> <owl:intersectionOf rdf:parseType="Collection">
> <owl:Class>
> <owl:complementOf>
> <owl:Restriction>
> <owl:onProperty
> rdf:resource="owl:topObjectProperty"/>
> <owl:someValuesFrom rdf:resource="#b"/>
> </owl:Restriction>
> </owl:complementOf>
> </owl:Class>
> <owl:Restriction>
> <owl:onProperty
> rdf:resource="owl:topObjectProperty"/>
> <owl:allValuesFrom rdf:resource="#b"/>
> </owl:Restriction>
> </owl:intersectionOf>
> </owl:Class>
> </owl:equivalentClass>
> </owl:Class>
>
> <!-- http://www.w3.org/2002/07/owl#Thing -->
>
> <owl:Class rdf:about="&owl;Thing"/>
> </rdf:RDF>
> <!-- Generated by the OWL API (version 2.2.1.1138)
> http://owlapi.sourceforge.net -->
>
> In your ontology instances of the class C cannot have any successors (there
you used the real top property) and instances of class Last cannot have any
http://www.semanticweb.org/ontologies/2009/9/O3.owl#TopObjectProperty
successor, but can have other successors.
>
>
> finally, I was wondering if there is a formula containing a
> topObjectProperty that is, say unsatisfiable, and if all occurences of
> topObjectProperty are substituted by another property R, then it becomes
> satisfiable. So, what I 'm asking is if there's an example which clearly
> shows the distinction between a topObjectProperty and an ordinary property,
> also I'm interested in logic (or maybe DL) based satisfiability, and not
> satisfiability based on domain, range or something else.
>
I was told that domain closure formulas such as \forall x.(F(x) <=> (x=a |
> x=b)), can be used to distinguish between the topObjectProperty and other
> properties, so this formula should be unsatisfiable:
> C(a) & C(b) & \forall x (C(x) <=> x=a)
>
This just implies a=b, unless you have unique name assumption.
> which is equivalent to:
> Ex.(C(x) & x=a) & Ex.(C(x) & x=b) & Ax.( (C(x) & x=a) | (~C(x)
> & ~x=a) )
> So I translated them to a DL called ALCO+U, which allows nominals and the
> Universal Role, using the translation:
> Ex.C(x) becomes in DL \exist U. C
> Ax.C(x) becomes in DL \forall U. C
> where U is the universal role.
Again, no need for the universal role:
C(a)
C(b)
C equals {a}
in functional style syntax
ClassAssertion(C a)
ClassAssertion(C b)
EquivalentClasses(C ObjectOneOf(a))
> And the other translations are straightforward, such as x=a becomes {a},
> and so on..
> Also, we assumed Unique Names Axioms in the above formula, but we need to
> explicitly mention that in OWL 2, so I used the DifferentIndividuals axiom
> to say that 'a' and 'b' are different individuals.
> This is that formula in Manchester Syntax:
> topObjectProperty some (C and {a})
> and topObjectProperty some (C and {b})
> and topObjectProperty only ((not C) or {a})
>
> So, after saying that 'a' and 'b' are distinct individuals, the formula is
> found unsatisfiable, which is correct, but when replacing topObjectProperty
> with another property, say R, the unsatisfiablility stays, which after some
> thinking I found it correct too. So this result made me write this email to
> ask for advice about whether the topObjectProperty can be distinguished from
> another role R using purely FOL semantics.
>
Well, it can be axiomatised, so you can replace the top object property by a
fresh property and add a couple of axioms (the fresh property is a super
property of all other axioms, etc.) and you have the same effect.
You should use the top object property sparsely, because it can be
computationally expensive and in all your examples it was not needed and
rather the result of a wrong translation, so I suggest you read more about
OWL semantics and maybe its relation to FOL. Maybe the OWL primer is
helpful:
http://www.w3.org/TR/owl2-primer/
Best regards,
Birte
>
> Thank you.
>
> Wael
>
--
Dr. Birte Glimm, Room 306
Computing Laboratory
Parks Road
Oxford
OX1 3QD
United Kingdom
+44 (0)1865 283529
Received on Thursday, 5 November 2009 17:40:28 UTC