questions about the topObjectProperty

View: New views
3 Messages — Rating Filter:   Alert me  

questions about the topObjectProperty

by wyehia :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message

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. 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.
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))          
which is equal to:    \forall x.False
I am not sure if this formula is satisfiable, maybe if the domain is empty. 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

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. 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. 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

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#" >
    <!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 -->





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)
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. 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.

Thank you.

Wael


Re: questions about the topObjectProperty

by Timothy Redmond :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message


I hope that this post is not misplaced but I thought I would give some  
context about the Protege reference.  Protege 4.0 is currently in  
transition and does not fully support OWL 2.0.    Roughly speaking  
Protege 4.0 supports OWL 1.1.  Protege 4.1, which will be released as  
an early alpha soon, does support OWL 2.0 and works with Hermit.

-Timothy


On Nov 4, 2009, at 7:30 PM, Wael Yehia wrote:

> 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. 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.
> 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))
> which is equal to:    \forall x.False
> I am not sure if this formula is satisfiable, maybe if the domain is  
> empty. 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
>
> 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. 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. 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
>
> 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#" >
>     <!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 
>  -->
>
>
>
>
>
> 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)
> 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. 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.
>
> Thank you.
>
> Wael
>



Re: questions about the topObjectProperty

by Birte Glimm :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message



2009/11/5 Wael Yehia <wmyehia2001@...>
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#" >
    <!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